Revision #2498 → #2738 · back to history
addedSecond-order logic (as extension of first-order logic)7336d0168e84
addedSecond-order quantification over relations155f535ec639
addedLaw of excluded middle as a second-order sentencec169758ac54f
addedDomain of discourse0b68974e5c40
addedQuantifying over individuals (first-order)bc82089abeb2
addedQuantifying over predicates (second-order)8201f14f12cf
addedSet of cubes and tetrahedrons34261e761f0e
addedNo dodecahedrons in the setb50dce016a0d
addedAncestor relation via second-order quantificationdb28bc72beea
addedNo second-order variables for properties of predicatesfdc0262d64c8
addedEquality (Leibniz's law)9f4fc994843f
addedSecond-order induction axiom4a9e95537523
addedSort of set (unary relation) variables9674fdbc3cf3
addedSort of k-ary relation variables416e5eb0bfb5
addedSort of k-ary function variables5e6cc0fddef8
addedSentence in second-order logic95991a516292
addedFunction variables reducible to relation variables3df806c63bb8
addedWeak second-order logic (WSO)568757396e76
addedMonadic second-order logic (MSO)7bf3116ee351
addedFull second-order logic57c39466bc30
addedDecidability of the MSO theory of the infinite binary tree (S2S)57aac2c19e8c
addedUndecidability of full second-order logic over infinite domains98df8df30051
addedFirst-order formula within second-order logic794cc27d47a2
addedExistential second-order formula5d98a6e0b04d
addedExistential second-order logic (ESO)87dd124de107
addedUniversal second-order logic52719383d09d
addedHigher fragments defined by mutual recursion04035e0b01b8
addedStandard (full) semanticsbb7f69cb5aee
addedFull modelebcbf89f77bc
addedHenkin semanticsf1a81be7014c
addedHenkin's completeness and compactness theorem2dd33d765617
addedHenkin models as disguised first-order models (Lindström)6a300af52213
addedNon-standard interpretations as a consequence of Gödel's incompleteness theorema0e318e9de3a
addedAdditive inverse expressible in first-order logicbbc66a5d41b2
addedLeast-upper-bound propertydf25af09be79
addedCategoricity of ordered fields satisfying the LUB property5b152057858b
addedLUB property not first-order expressibleac79ce77e74f
addedReal-closed fields share first-order theory with the reals88e7c0be52f0
addedFiniteness expressible in second-order logic613ccded63f5
addedCountable cardinality expressible in second-order logicb9a987ce7a6d
addedFiniteness/countability not first-order expressiblefd22bac17e04
addedESO fragment more expressive than first-order logic9e20ae7bfc35
addedDeductive systemfb3df1b73c7c
addedNo deductive system complete for standard semantics82700fc062b4
addedWeakest deductive system for second-order logic588588cf68e2
addedSoundness of comprehension and choice axioms73fa0fca85f8
addedAttempted reduction to a two-sorted first-order theoryff98567a513e
addedLöwenheim–Skolem construction of internal numbers/setsd13daebaed23
addedInternal numbers fail the full least-upper-bound axiom701ecb778f6a
addedUniqueness of the Archimedean complete ordered fieldf3a110647cac
addedSecond-order theory of the reals not reducible to first-order theorya6aa160af1b1
addedContinuum-hypothesis-dependent second-order theoryf6f0f813911d
addedNo sound, complete, effective deductive system for full second-order logic472b6d73efa8
addedHenkin's completeness theorem for Henkin semantics60c536b574b9
addedCompactness and Löwenheim–Skolem fail for full models66130b0e255a
addedBüchi–Elgot–Trakhtenbrot theorem6f43a966a63b
addedFagin's theorem0dd31eb1d764
addedco-NP characterized by universal second-order formulas2943a19c515f
addedPH characterized by second-order formulas2793c232248c
addedPSPACE characterized by second-order formulas with transitive closureeee4592843ce
addedEXPTIME characterized by second-order formulas with least fixed point95f228cdaea5
addedPH = PSPACE consequence for transitive closure expressivenessc4d0fcdb6d67