Start with the propositional variables as atomic symbols and close under the two formation operations
The set of propositional formulas is the smallest set satisfying these conditions: every logical formula has a finite construction from logical variables by negation and logical implication, and no other strings qualify. In particular, parentheses belong to the binary logical implication formation rule; they cannot be added or removed arbitrarily. Each symbol is one token, regardless of how its index is printed.
Use structural induction on the formation of a propositional formula. A propositional variable has no parentheses. Applying negation to a logical formula adds no parentheses, so preserves equality of the two counts. If and each have equally many opening and closing parentheses, the formation of adds one of each to their combined counts. Thus every propositional formula satisfies
This is a necessary condition for being a logical formula; it is not sufficient, since the logical connectives and the placement of symbols must also follow the formation rules.
Not a logical formula. The string has one opening parenthesis and no closing parenthesis, contradicting the parentheses count established above. It also fails the binary logical implication formation rule, whose final symbol must be a closing parenthesis.
Not a logical formula of this language. Logical disjunction is not one of its permitted logical connectives. Even though the displayed expression has an ordinary interpretation in a larger propositional language, membership in the specified formal language is a syntactic question. A logically equivalent logical formula using only negation and logical implication would have to be written with those symbols instead.
A logical formula. Both and are propositional variables, so and are logical formulas. Applying the binary logical implication formation rule to this ordered pair of logical formulas gives the displayed whole expression. This supplies a construction of its formula syntax tree rather than merely checking that its parentheses balance.
The unique readability theorem says that every propositional formula has exactly one of the following forms: a unique propositional variable; for a unique logical formula ; or for a unique ordered pair of logical formulas . These three alternatives are disjoint. Consequently each logical formula has a unique formula syntax tree and a uniquely determined principal logical connective whenever it is not a logical variable.
A propositional variable is a single symbol of the alphabet. Its only nonempty substring is that symbol itself. Every propositional formula is nonempty, so the only substring that is a logical formula is . Therefore
The subscript is part of the name of an atomic token; it does not introduce additional symbol positions inside the logical variable.
A useful consequence of the formation rules is that logical formulas form a prefix-free set of strings. To see this, describe a deterministic parser that reads one logical formula from its starting position. On a logical variable it consumes that one symbol. On a negation symbol it recursively reads one following logical formula. On an opening parenthesis it recursively reads a left logical formula, requires a logical implication symbol, recursively reads a right logical formula, and requires the closing parenthesis. Induction on formation proves that, if a valid logical formula begins at the current position, this procedure consumes exactly that logical formula and stops at its end.
Suppose now that both and are logical formulas and . The same parser, started at their common first symbol, must stop both at the end of and at the end of . Its deterministic stopping position cannot differ, so is empty. Hence
This argument applies to symbol strings; it does not use truth values or logical equivalence.
First note that a substring which is itself a logical formula must coincide with a subtree of the formula syntax tree of the surrounding logical formula. Indeed, a logical formula can begin only at a logical variable, a negation symbol or an opening parenthesis. Every such position in a valid logical formula is the start of one of its parsed subtrees. If is the logical formula at that subtree and is another logical formula starting at the same position, one is an initial segment of the other; prefix-freeness of fully parenthesized formulas from the preceding part forces .
Now consider a final subformula. For a logical variable, it can only be the whole logical formula. For a binary logical implication , every proper subtree is contained in or and finishes before the final closing parenthesis of the whole expression. It therefore cannot be a final substring of the whole. The only remaining possible outer formation is negation. Thus
The second alternative is a necessary possibility, not a claim that every negated logical formula has every one of its subformulas as a suffix.
The whole logical formula is a subformula of itself, and any subformula of remains a contiguous substring after placing a negation symbol in front of .
Conversely, a subformula occurrence starting at the first symbol of is an initial subformula, so equals the whole logical formula by prefix-freeness of fully parenthesized formulas. An occurrence starting later lies wholly inside the following string , and is therefore a subformula of . Consequently
Here records distinct logical formulas; multiple occurrences of the same logical formula do not create different elements of this set.
A subformula beginning at the first opening parenthesis equals the whole logical formula by prefix-freeness of fully parenthesized formulas. Every other subformula is the logical formula of a proper syntax subtree, by the parsing argument in part (iii). The two children of the root are precisely and , so such a subtree lies entirely inside one of those children. In particular no logical formula substring can begin in and cross the principal logical implication symbol into .
Conversely, each subformula of either child is visibly a substring of the whole expression, as is the whole expression itself. Thus
Together these cases identify the substring definition of a subformula with its usual syntax-tree definition.
Fix the particular occurrence of that is being replaced. The subformula analysis above makes it a node of the formula syntax tree of . Proceed by structural induction on the surrounding logical formula.
If this node is the root, the subformula replacement gives , already a logical formula. Otherwise, if , the chosen occurrence lies inside . The induction hypothesis gives a logical formula after the subformula replacement there, and the whole result is the logical formula . If , a proper chosen occurrence lies in exactly one of the two children. Replacing inside that child gives either or , each a logical formula by the formation rule. A logical variable has no proper subformula, so there is no additional base case.
Therefore replacing the designated subformula occurrence by any logical formula preserves well-formedness. The argument concerns one chosen occurrence; it does not require simultaneous subformula replacement of every occurrence of the same string.
Fix any Boolean valuation . Logical equivalence of and means for this Boolean valuation and every other one. Follow the unique path from the replaced node to the root of the formula syntax tree. At a negation node, equal input truth values have equal negations. At a logical implication node, the unaffected child has the same truth value before and after subformula replacement, while the affected child has the same truth value by induction; the resulting logical implications therefore agree as well.
Induction along that finite path yields . Since was arbitrary,
This is the replacement theorem for logical equivalence: the semantics of each logical connective depends only on the truth values of its immediate inputs.
A collection of logical connectives is functionally complete, or adequate, if every Boolean function of finitely many propositional variables is represented by a logical formula using only those logical connectives. More explicitly, for every and every there is a logical formula whose truth value under each Boolean valuation is . Constant functions with Boolean values may use an otherwise irrelevant logical variable, for example for truth and for falsity.
Translate logical formulas recursively, leaving propositional variables unchanged and translating negation by applying negation to the translation. For the other two logical connectives set
The first logical implication is false exactly when both original inputs are false; the second displayed logical formula is true exactly when both inputs are true. Hence each clause preserves truth values. Structural induction gives for every Boolean valuation and every logical formula in the larger language.
By the assumed functional completeness of negation, logical conjunction and logical disjunction, any finite Boolean function has such a logical formula . Its translation uses only negation and logical implication and represents the same function. Thus is adequate.
Under any Boolean valuation there are two possibilities. If is false, the outer logical implication is true by vacuous truth. If it is true, then is false, which forces true and false. In that case is true, so the outer logical implication is again true. These possibilities exhaust the truth values of its antecedent; therefore
There is a three-line Hilbert formal proof. Use A1 with , ; then use A3 with , :
This is a direct logical derivation in the displayed Hilbert proof system. Neither the deduction theorem for propositional logic nor a completeness theorem for propositional logic is needed: the desired logical implication is just the contrapositive, supplied by A3, of the particular A1 instance on line 1.
Yes, for soundness and completeness of theoremhood. An axiom-only complete propositional calculus is obtained as follows. Declare every propositional tautology, and only such a tautology, to be an axiom; supply no inference rules. A formal proof then consists of a single axiom. Every proved logical formula is valid, giving soundness, and every valid logical formula is already an axiom, giving completeness.
This is not merely an unspecified collection: whether a finite propositional formula is a tautology is decidable by its finite truth table, so the axiom set can be recognized effectively. It is a deliberately uninformative Hilbert proof system, since all the work has been put into axiom recognition. If one instead asked for strong completeness of derivations from arbitrary additional assumptions, a system whose only formal proof lines are axioms or assumptions would not suffice; the affirmative construction here concerns versus .
An -structure consists of a nonempty domain , an element for each constant symbol, a function for each -ary function symbol, and a relation for each -ary predicate symbol. When equality is part of the logic it is interpreted as actual identity on .
An assignment in a first-order structure is a function from logical variables to . It induces a term valuation of first-order terms recursively:
For an atomic formula, substitute these first-order term values into the interpreted relation, or compare them for equality. Extend satisfaction for a set structure through the truth tables of the logical connectives, and through the quantifier clauses
Thus the first-order structure and assignment in a first-order structure together determine truth values for all logical formulas. A first-order sentence has no free variables, so its truth does not depend on the assignment in a first-order structure.
The assertion that is a first-order model of means that every first-order sentence belonging to is true in the first-order structure:
Equivalently each first-order sentence is true under every assignment in a first-order structure, since first-order sentences have no free variables. The first-order sentences must all hold in the same interpretation of the language; one cannot select a different first-order structure for each member of .
Use the following group axioms in the given language:
Commutativity supplies the other identity and inverse equations. These first-order sentences therefore specify precisely an abelian group with the named identity ; an inverse function symbol is unnecessary because inverses are asserted to exist by a quantified formula.
For each positive integer , let be the first-order term recursively defined by and . Add the torsion-free abelian group axiom scheme
Every first-order model of these first-order sentences is an abelian group with no nonidentity element of finite order. Conversely every torsion-free abelian group satisfies each of the displayed first-order sentences. This is a countably infinite first-order axiomatization of exactly the required class.
No finite axiomatization exists. Write for the axioms just constructed and suppose a finite set of first-order sentences had exactly the same first-order models. Its logical conjunction is a single first-order sentence, and . By the compactness theorem there is a finite subset with : otherwise would be finitely satisfiable and hence satisfiable, a contradiction.
Only finitely many of the integers in the torsion-free scheme occur in . Choose a prime number larger than all of them. The cyclic group satisfies all the group axioms and each of these finitely many conditions from the torsion-free abelian group axiom scheme: multiplication by an integer is invertible modulo , so implies . It consequently satisfies , then , and therefore .
But its nonzero elements have finite order , so it is not a torsion-free group, contradicting the assumed description of the first-order models of . This establishes the nonfinite axiomatizability of torsion-free abelian groups, ruling out every finite set of defining first-order sentences, not just finite subsets of the particular scheme in part (c).
For a standard classical propositional calculus, strong completeness states
Together with soundness, this identifies semantic consequence with formal derivability. One proves the contrapositive by the maximal consistent set in propositional logic construction. If , the set is propositionally consistent, by the deduction theorem for propositional logic and classical propositional reasoning. Extend it to a maximal consistent set in propositional logic , deciding each logical formula in turn. At each stage at least one selection of or preserves propositional consistency; a contradiction in the union would use only finitely many assumptions and hence already occur at a stage.
Define a Boolean valuation by exactly when . Maximal consistency in propositional logic gives exactly when , and exactly when either or . Structural induction on logical formulas therefore proves the maximal consistent set truth lemma . Thus satisfies but falsifies , contradicting semantic entailment. The countable language here permits an enumeration of logical formulas; the corresponding general-language argument uses a well-ordering or a principle of maximality in a partially ordered set.
Gödel's completeness theorem for first-order sentences says that, in a standard sound first-order Hilbert calculus,
Equivalently every first-order consistent set of first-order sentences has a first-order model: apply this existence statement to for the consequence formulation.
For the first-order model existence formal proof use a Henkin construction. Enlarge the language by fresh constant symbols and adjoin Henkin witness axioms
Freshness of preserves first-order consistency. In detail, if a contradiction followed after adjoining one witness axiom, the deduction theorem for first-order logic would yield its negation, from which one obtains both and over the old theory. Since the new constant symbol does not occur in that theory or in , replace it by a fresh logical variable and generalize to derive , a contradiction. Finitely many witness additions preserve first-order consistency successively, and unions preserve first-order consistency because formal proofs are finite. Iterate the enlargement so that logical formulas involving newly introduced constant symbols also receive witnesses. Include at least one constant symbol to guarantee closed terms.
Extend the resulting first-order consistent witnessed first-order theory to a maximal consistent set of first-order sentences . In the equality-free case make the domain the set of closed terms. Interpret constant symbols and function symbols by their formal first-order term constructions; interpret an atomic formula by
The truth lemma for a Henkin term model follows by induction on logical formulas with closed terms substituted for their free variables. The logical connective steps use maximal consistency of a first-order theory. In the existential step, membership of supplies a witness constant and hence a first-order term satisfying ; conversely a satisfying closed term gives the existential sentence by an inference of the calculus. The term model consequently satisfies and the original theory. Equality is absent here, so distinct closed terms may remain distinct domain elements without further identifications.
In the presence of equality, two syntactically different closed terms can be asserted equal by the Henkin theory, so the raw first-order term domain from part (b) must be replaced by a quotient set. Define
The equality axioms give reflexivity, symmetry and transitivity, so this is an equivalence relation. Their substitution consequences make it a congruence relation on a first-order structure: replacing an input by an equivalent first-order term preserves equivalence of function values and preserves membership of atomic formulas in .
Take domain . Define a function symbol by , and relations by the same membership test as before using representatives. The congruence relation on a first-order structure makes these definitions independent of representatives. Actual identity of equivalence classes now agrees with the formal equality first-order sentences in :
This supplies the equality case of the truth lemma for a Henkin term model; the logical connective and quantifier cases then proceed exactly as in the Henkin construction. Thus the term model built from the quotient set is a genuine first-order model with equality interpreted as identity.
For a countable first-order language, the Henkin construction introduces only countably many constant symbols: each round needs at most one for each logical formula, there are countably many finite strings in a countable alphabet, and countably many rounds suffice. There are therefore at most countably many closed terms. The term model, and also its quotient set by equality, has at most countably many elements.
It follows that every satisfiable theory in a countable first-order language has an at most countable first-order model. If the theory has no finite first-order model, the constructed first-order model is countably infinite. More generally the same counting argument gives a first-order model of cardinality at most for any satisfiable theory in language .
For the elementary-substructure version of the downward Löwenheim-Skolem theorem, begin with a first-order structure and a set of designated elements. Close , the named constant symbols and one initial element under the language's functions and under chosen witnesses in for existential formulas with parameters already chosen. Iterate countably often. The resulting set has cardinality at most , and its induced substructure is elementary: induction on logical formulas proves the truth equivalence, with the existential case supplied by the chosen witnesses. This is the same witness mechanism as the Henkin formal proof, now keeping witnesses inside a given first-order model.
Let in the finite language of rings: it is the set of all first-order sentences true in the field of complex numbers. It is satisfiable, with first-order model , so the countable-language Löwenheim-Skolem theorem gives an at most countable first-order model of .
All field axioms belong to , hence is a field. For every positive integer , the first-order sentence saying that there are at least distinct elements is also true in and belongs to . Thus cannot be finite, and is countably infinite.
Finally, for each first-order sentence , either or . Since satisfies all of , it satisfies exactly when does. Therefore
Elementary equivalence concerns first-order first-order sentences and does not imply an isomorphism; the two fields have different cardinalities. The stronger downward form may even choose as a countable elementary subfield of .

Articles by others on the same topic (0)

There are currently no matching articles.