Main properties of propositional logic

Propositional calculus has several different ways to “validate” propositions: deduction systems that demonstrate theorems and semantic methods that define tautologies. The question that arises is whether these methods coincide.

Decidability, coherence, completeness, compactness

The fact that any proposition is demonstrable if it is a tautology expresses a property of the propositional calculus which is called completeness, this means that the deductive presentation of the propositional calculus is equivalent to the semantic presentation. Completeness is based on the following remarks.

• Any demonstrated proposition results from an axiom or from the application of a rule to propositions that have already been demonstrated. Now it is easy to verify that the axioms provide tautologies and that the rules preserve the tautologies. Every demonstrated proposition is therefore a tautology. The propositional calculus is correct.
• The converse relies on the following fact: one can demonstrate that for any proposition P of the propositional calculus there exists a proposition P′ such that P ↔ P′ and such that P′ is in a so-called normal form Q₁ ˄ Q₂ ˄ … ˄ Q_n where each Q_i is of the form R₁ ˅ R₂ ˅ … ˅ R_k , where each R_i is a literal (i.e. a proposition of the form p or ¬p ). If P′ is a tautology, then in each Q_i, necessarily appear a propositional variable p and its negation ¬p . Otherwise there would exist Q_i which would not satisfy this condition and it would be possible to assign values ​​to p_j so as to give the value 0 to Q_i, and therefore to P′ itself. But one can show that p ˅ ¬p is demonstrable (⊢ p ˅ ¬p ), then that it is the same for each Q_i, then for P′ itself and finally for P. Any tautology is then demonstrable. The propositional calculus is complete.

The completeness theorem of propositional calculus offers another more detailed proof.

It follows from the completeness of the calculation of the propositions that:

• The calculus of propositions is decidable, in the sense that there is an algorithm to decide whether a proposition is a theorem or not. It suffices to draw up its truth table and see if it is a tautology.
• The calculation of the propositions is coherent (consistent), that is to say not contradictory. There is no proposition P such that we can have ⊢ P and ⊢ ¬ P at the same time because these two propositions would be tautologies and we would have 1 = 0.
• The calculus of propositions is strongly complete (maximally consistent), in the sense that any addition of a new axiom schema, not provable in the initial system, makes this system inconsistent.

Suppose given an infinite number of propositions. Can these propositions be simultaneously satisfied? That is, are there truth values ​​for their propositional variables that give 1 as the truth value to all propositions? If the answer is positive for any finite subset of these propositions, then it is for all the propositions. This property, which ensures that one can pass from all finite subsets to the entire infinite set, is called compactness.

Calculation methods, NP-completeness

We have seen that, to decide if a proposition is classically provable, it suffices to check whether it is a tautology, i.e. to check whether it takes the truth value 1 whatever the truth values ​​of its propositional variables.

However, this brutal approach comes up against the calculation time it requires. Indeed, if the proposition has n propositional variables, it is necessary to calculate 2n possible combinations of values ​​for the propositional variables, which quickly becomes infeasible for large n. Thus, if n = 30, it will be necessary to enumerate more than a billion combinations of values.

There are certainly possible improvements. For example, if we assign the truth value 0 to a propositional variable p, we can directly assign the value 0 to p ˄ q independently of the subsequent value assigned to q, which reduces the number of calculations to be performed.

One can also look to see if it is possible to invalidate the implications. Consider for example the proposition:

( ( p → ( q ˄ r ˄ s ) ) ˄ ¬s ) → ¬p

Being made up of an implication, to make it invalid, it suffices that the conclusion ¬p can take the value 0 (and therefore p the value 1) and that the hypothesis ( ( p → ( q ˄ r ˄ s ) ) ˄ ¬s) can take the value 1 (and therefore ¬s and p → (q ˄ r ˄ s) the value 1). But then s takes the value 0 and (p → (q ˄ r ˄ s) can only take the value 0. It is therefore impossible to invalidate the implication and this one is a tautology.

But the previous improvements do not fundamentally change the difficulty of the problem. We are therefore faced with the following situation. Given a proposition f, one asks whether f is a tautology or not and for this one asks whether there are truth values ​​attributable to the propositional variables of f that would make f invalid.

• An exhaustive search requires 2n checks if f has n propositional variables. This approach is called deterministic, but its computation time is exponential.
• On the other hand, if f is not a tautology, it is enough to make a verification, namely to test precisely the configuration which invalidates f. This verification requires a simple Boolean calculation, which is done in polynomial time (essentially linear in fact). The calculation time therefore ceases to be exponential, on condition of knowing which configuration to test. This could, for example, be given by an omniscient being who is not completely trusted. Such an approach is said to be non-deterministic.

The question of the invalidity of f, as well as all the problems which are solved according to the method which we have just outlined, are said to be NP (for nondeterministic polynomial). Testing the invalidity of f is equivalent by very simple calculations (in polynomial time) to testing the satisfiability of its negation. The problem of the satisfiability of a proposition, namely finding a configuration which gives 1 as the truth value of the proposition is called the SAT problem (from the boolean SATisfiability problem). It plays a fundamental role in complexity theory, since it can be shown that the discovery of a deterministic algorithm in polynomial time for this problem would make it possible to deduce deterministic algorithms in polynomial time for all problems of the NP type (theorem of Cook). We say that SAT (and therefore also the problem of the non-provability of a proposition) is an NP-complete problem. The problem of the demonstrability of a proposition is said to be co-NP (for complement of NP).

The SAT problem in fact most often designates that of the satisfiability of a conjunction of clauses (a particular case among the propositions), but the problem of the satisfiability of a proposition is brought back to this one by a polynomial reduction (a put in clausal form by equisatisfiability, those by logical equivalence do not work).

Boolean algebra

Let E be the set of propositions over a set of propositional variables. The binary relation defined on E by the (classical) equivalence between two propositions is denoted ≡. It is an equivalence relation on E, compatible with conjunction (which gives the lower bound of two elements), disjunction (which gives the upper bound of two elements), and negation (which gives the complement). The quotient set E/_≡ of the propositional calculus.

As soon as the set of propositional variables is infinite, the Lindenbaum algebra of propositional formulas has no atoms, i.e. no minimal nonzero element (for any formula which is not an antilogy, we get a strictly inferior element by conjunction with a propositional variable not present in the formula). This distinguishes it from the Boolean algebra of all parts of a set, which has the singletons of the set as atoms.

Heyting algebras were defined by Arend Heyting to interpret intuitionistic logic.

Conjunctive normal forms, disjunctive normal forms

A disjunction is a proposition of the form p ˅ q and a conjunction is a proposition of the form p ˄ q. A clause is in conjunctive normal form (CNF) if it is composed of conjunctions of disjunctions. A proposition is in disjunctive normal form (DNF) if it is composed of disjunctions of conjunctions.

Examples:

• p, ¬p, p ˅ q and p ˄ q are both FNCs and FNDs.
• (p ˅ q) ˄ (¬p ˅ r) ˄ s is in conjunctive normal form.
• (p ˄ q ˄ r) ˅ (¬p ˄ ¬s) ˅ ¬q is in disjunctive normal form.

When each disjunctive block of a DNF comprises one and only one occurrence of the same propositional variables, we then speak of a distinguished DNF.

When each conjunctive block of a NCF has one and only one occurrence of the same propositional variables, we then speak of a distinguished NCF.

Examples:

• (p ˅ q ˅ r) ˄ (¬p ˅ ¬q ˅ r) ˄ (¬p ˅ ¬q ˅ ¬r) is in distinguished conjunctive normal form.
• (p ˄ q ˄ r) ˅ (¬p ˄ q ˄ ¬r) ˅ (¬p ˄ ¬q ˄ r) is in distinguished disjunctive normal form.

We can show that any proposition is equivalent to an NDF (assuming that ⊥ is the disjunction of an empty set of propositions) and is equivalent to an FNC (assuming that T is the conjunction of an empty set of propositions). That is, for any proposition p there exists a proposition q in disjunctive normal form such that p ↔ q and a proposition r in conjunctive normal form such that p ↔ r.

(Includes texts from Wikipedia translated and adapted by Nicolae Sfetcu)