Revision #141 → #1226 · back to history
addedFirst-order logic54127aa47a79
addedFirst-order vs higher-order logicd0587a299a73
addedPredicateb07b4ebcb9dc
addedInterpretation (model)2856ee45db0a
addedTerms and formulase90e0f7ff8a8
addedLogical and non-logical symbols40a38f3849d2
addedSufficiency of symbolsefde7466f50c
addedSignaturee9fc9f84e744
addedPredicate symbola13a1dca5212
addedFunction symbolc33fcedb6430
addedConstant symbol28818b2d1f6e
addedFormation rulese62c25b4eefd
addedFormulas (well-formed formulas)486b788ef2ca
addedAtomic formulase9cfe03b9eaf
addedUnique readability of formulasea7cdb43c419
addedOperator precedence conventionsc2bc845d1f47
addedFree and bound variables22c2f4efbd22
addedFirst-order sentence8ef23ad25cd8
addedLanguage of ordered abelian groupsbc5da5676233
addedInterpretation of a first-order languageb356fd82a265
addedStructure (model)53616826c07b
addedDomain of discourse03b2b8f53d40
addedInterpretation of non-logical symbols0a288eec7dc5
addedVariable assignmente88716235d5a
addedT-schemad644b83c0e65
addedAlternate truth definition71c735415357
addedEquivalence of truth definitionsb391d908223d
addedSatisfiabilityd47db9ace88e
addedSatisfiability with free variables720a9b9f7dd1
addedLogically valid formulaec8bcc26a125
addedLogical consequence4890fb94e0d1
addedTarski–Givant relation algebra equivalencec5e0719c8424
addedFirst-order theory16debb48f9d8
addedModel and elementary class0a303f393bcb
addedExistence of nonstandard models7b4667918521
addedConsistent and complete theoryeb75d0d7f2f0
addedGödel's incompleteness theoremeb6708778662
addedEmpty domains and rules of inferenceae34288162cd
addedDeductive system8b7d26edce2a
addedSound and complete deductive systemffaf9e3942df
addedSemidecidability of logical consequence8423a4bca2ff
addedRule of inference2ff45f02b8ae
addedSubstitution rule1c5bafe4a148
addedHilbert-style deductive systemf0a7acd27f39
addedNatural deduction systems9d4060ade0f2
addedTableaux methodbcd9930dee60
addedResolution rule sound and complete3b80ade23914
addedProvable identities6f284f4e8e47
addedFirst-order logic with equalityf0008dc702ca
addedReflexivity axiom160dc7f03a6d
addedSubstitution for functions axiom468f30cc9702
addedSubstitution for formulas (Leibniz's law)ca453621c3d0
addedSymmetry and transitivity of equality86477e25915f
addedFirst-order logic without equalityd960d7bc06ab
addedNormal modelbe259869ceac
addedTheory with equalityce0ccb90e1e5
addedAd hoc definitions of equalityf0d2c39e9338
addedGödel's completeness theorem0258afc7ee5b
addedSemidecidability of first-order consequence456691e2366b
addedUndecidability of first-order logic39d361655128
addedDecidable fragments existe3671c6180e7
addedTwo-variable counting fragment C2dd55a8670ed5
addedMonadic first-order fragmentb7073a3bb0b8
addedLöb–Gurevich fragmente8c5f466340a
addedRabin fragment48a4e3334d20
addedBernays–Schönfinkel–Ramsey fragmentdbdf3426734c
addedLöwenheim–Skolem theorem4484897db56b
addedInfinite structures not categorically axiomatizablecafea59c1beb
addedCompactness theorem0e0504d3ff29
addedFinite graphs not an elementary class23e0d228d1bb
addedConnected graphs not an elementary class1d046822aa42
addedLindström's theoremd8811bfda74f
addedNo categorical first-order theory with infinite model070cf8cddea0
addedFormalizing natural languageb3153dbf002c
addedReducing logical symbolsa1dffe30f230
addedEliminating function and constant symbols7553f8cccf39
addedRestricting arities via pairing function0ac63fe4f9ea
addedMany-sorted first-order logicdecf4503e94f
addedReduction to single-sorted logic4773e97f0012
addedUniqueness quantificationd8dba0391f7e
addedExtra quantifiersa988070d5436
addedInfinitary logicf22f04a39737
addedInfinitary logic notation L_αβ27a01a968b3b
addedIntuitionistic first-order logiceb227c765b7c
addedFirst-order modal logic8c0ed57379c7
addedFirst-order fuzzy logics32606126afcf
addedFixpoint logic0e8d472129c8
addedSecond-order logic5698c463aecf
addedSecond-order consequence not semidecidable46294de6cfae
addedMetalogical theorems fail in higher-order logic341f822f16fb
addedAutomated theorem proving63c26472bf65
addedModel checking for first-order logic1e1acf09388f