A Boolean valuation is an arbitrary function assigning one of the two truth values to each propositional variable. It extends uniquely to all propositional formulas by following the construction of the propositional formula:For logical implication, is false exactly when is true and is false; otherwise it is true. Here the operations on the right are Boolean operations on truth values. Structural recursion gives existence, and structural induction gives uniqueness: once the immediate subformulas have their values, the outer connective fixes the resulting value.
Two propositional formulas are logically equivalent if every Boolean valuation gives them the same truth value. A disjunctive normal form is a logical disjunction of logical conjunctions of literals, with a literal being a propositional variable or its negation.
Let include all propositional variables appearing in . For each Boolean valuation , putThe minterm is true exactly for Boolean valuations whose restrictions to these propositional variables are . ConsequentlyIndeed, an Boolean valuation making true makes its own minterm true, while a true minterm in the displayed logical disjunction certifies the truth of . There are only finitely many Boolean valuations, so this is a finite disjunctive normal form. If there are no satisfying Boolean valuations, use for any propositional variable ; this is a disjunctive normal form for falsity without needing an empty logical disjunction convention.
Assume first that is false on the all-true and all-false Boolean valuations. Use the truth-table normal form from part (ii). Every satisfying Boolean valuation on the finitely many propositional variables must have at least one true propositional variable and at least one false propositional variable. Its minterm therefore has the formwhere conjoins its true propositional variables and disjoins its false propositional variables; both lists are nonempty. This is equivalent to . If the satisfying Boolean valuations are indexed by , De Morgan's laws givesIf there are no satisfying Boolean valuations, take and : the result is , again always false.
Conversely, on the all-true Boolean valuation every nonempty is true, so every is true. On the all-false Boolean valuation every nonempty is false, so every logical implication is again true. Negating their logical conjunction gives false on both Boolean valuations. Logical equivalence transfers these values to . The usual nonempty meaning of logical conjunction and logical disjunction of propositional variables is used here; allowing empty or without qualification would destroy this converse.
A logical derivation from is a finite sequence of propositional formulas, each either a member of , an instance of one of the three axioms, or obtained from earlier lines by one of the two displayed inference rules. The notation means that some such logical derivation ends in . Writing means derivability with no assumptions.
Propositional consistency means that there is no propositional formula for which both and . Equivalently not every propositional formula is derivable. To check the equivalence directly for this calculus, use the identity theorem proved in (ii): from and L3 obtain ; two uses of modus ponens rule give arbitrary . Thus a contradictory theory proves everything. Conversely a theory proving everything proves a propositional formula and its negation.
Choose an auxiliary propositional formula . The two instances of L1 areThe instance of L2 with isApply modus ponens rule first with the first L1 instance and then with the second. This is an assumption-free logical derivation, soIn particular no semantic completeness theorem or deduction theorem for propositional logic has been assumed to obtain this identity theorem.
An instance of L3 isUsing the first assumed logical derivation and modus ponens rule gives . The L2 instance for these same three propositional formulas isUse the other assumed logical derivation and then the newly obtained logical derivation in two applications of modus ponens rule. ThereforeThis conditional modus ponens construction is the step needed to discharge assumptions from a modus ponens rule line in part (iv).
For this calculus the deduction theorem for propositional logic isFor the reverse logical implication, retain the logical derivation from , add the assumption , and use modus ponens rule.
For the forward logical implication, induct on a logical derivation from . For each line we construct a logical derivation of from . If , use (ii). If is an axiom instance or belongs to , it is already derivable from ; L1 gives , and modus ponens rule finishes that case.
If comes by the elimination rule E from and , the induction hypothesis suppliesThe L2 instance with combines these by two applications of modus ponens rule. Thus the rule E also survives the discharge construction. These are all possible lines, proving the theorem for the final line .
Suppose both extensions were inconsistent. By the explosion argument in (i), the extension by proves , and the extension by proves . The deduction theorem for propositional logic therefore yieldsThe identity theorem gives and . Apply E to the first displayed logical implication and the identity logical implication with antecedent to obtain . Apply E to the identity logical implication with antecedent and the second displayed logical implication to obtain . This contradicts propositional consistency of .
Consequently at least one of the two one-formula extensions is propositionally consistent. The formal proof uses the source's own calculus, including its rule E, rather than assuming an unproved completeness theorem for this presentation.
The first-order terms are the smallest collection containing every variable and and containing whenever are first-order terms. The atomic formulas are exactly for first-order terms . Logical formulas are then obtained from atomic formulas by the logical connectives and quantifiers: if are logical formulas and a variable, then , , , , and are logical formulas. These closure rules, with no additional strings admitted, define the syntax; a presentation using fewer primitive connectives treats the others as abbreviations.
Semantic entailment is the conditionThe same first-order variable assignment is used for all premises and the conclusion. This matters when free variables occur; for first-order sentences the truth value is independent of the first-order variable assignment.
For independence, construct four first-order structures, each satisfying exactly the three required remaining axioms and failing the chosen one.
To fail associativity, use the carrier , interpret as , and define the commutative operation by its table:The first row and column give a two-sided identity, and every element is its own inverse because the diagonal entries are . Symmetry gives commutativity. Butso associativity fails.
To fail the identity axiom, take , , and the constant operation . It is associative and commutative, and every element has a two-sided partner producing ; but .
To fail the inverse axiom, use natural numbers under addition with . Addition is associative and commutative and has the required identity, but has no additive inverse in this carrier.
To fail commutativity, use the symmetric group under permutation composition with its identity. Associativity, identity and inverses are group properties, while . Each countermodel witnesses the failure of semantic entailment from the other three to the failed first-order sentence. Hence the four source axioms are independent.
Soundness states that formal derivability implies semantic entailment:For first-order sentences this means that every first-order structure satisfying all assumptions also satisfies every first-order sentence formally derived from them. In the logical formula version one uses the usual restrictions on generalization from assumptions with free variables.
Strong completeness states the converse:Equivalently, every syntactically consistent set of first-order sentences has a first-order model. Equality is interpreted as actual identity, and its usual logical axioms and substitution rules are part of the standard calculus. Both assertions hold for arbitrary sets of assumptions, rather than only finite sets.
The compactness theorem says that a set of first-order sentences has a first-order model if and only if every finite subset of has a first-order model. One direction follows by using the same first-order model for each subset.
For the nontrivial direction suppose every finite subset has a first-order model, but has none. Semantically , so completeness gives a formal logical derivation . A formal logical derivation is finite and uses only finitely many assumptions, say . Thus . Soundness would make unsatisfiable, contradicting the hypothesis. Here can be any fixed contradictory first-order sentence, such as , if it is not a primitive logical symbol. Therefore finite satisfiability implies satisfiability.
Take to consist of the three usual first-order sentencesThese assert reflexivity, symmetry and transitivity and therefore define exactly the equivalence relations.
For , adjoin to the single first-order sentenceIts witness gives a second member of each class, while its final universal clause excludes all others. Hence every class has exactly two members, and conversely such a relation satisfies it. This remains a finite set of first-order sentences.
For each positive integer , writeThenEvery class in a first-order model has at least elements for every , so cannot be finite. Conversely every infinite equivalence class supplies each finite collection of distinct witnesses. The displayed infinite scheme therefore has exactly the requested first-order models.
Suppose such a first-order theory existed. Add two new constants and considerwhere is the finite lower-bound logical formula from (iii).
Every finite subset of has a first-order model. Choose a first-order structure with exactly two equivalence classes: one countably infinite, and one finite of size at least the largest bound appearing in that subset. Interpret in the infinite class and in the finite class. The first-order structure satisfies all of , by its assumed characterization, and meets the finite demands on both named classes.
Compactness theorem in the language with the two new constants gives a first-order model of all of . Its classes of and are distinct and both infinite. Its reduct still satisfies , which is impossible if characterizes exactly one infinite class. HenceThe finite approximations work because any finite list of lower bounds permits the second class to remain finite; the entire list prevents that escape.
Articles by others on the same topic
There are currently no matching articles.