more on this theme
|
more from this text
Single Idea 9539
[filed under theme 4. Formal Logic / B. Propositional Logic PL / 5. Completeness of PL
]
Full Idea
A logical system is complete is all expressions of a specified kind are derivable in it. If we specify tautologous sequent-expressions, then propositional logic is complete, because we can show that all tautologous sequents are derivable.
Gist of Idea
Propositional logic is complete, since all of its tautologous sequents are derivable
Source
E.J. Lemmon (Beginning Logic [1965], 2.5)
Book Ref
Lemmon,E.J.: 'Beginning Logic' [Nelson 1979], p.90
A Reaction
[See Lemmon 2.5 for details of the proofs]
The
52 ideas
from E.J. Lemmon
|
13901
|
Predicate logic uses propositional connectives and variables, plus new introduction and elimination rules
[Lemmon]
|
|
9511
|
We write the conditional 'if P (antecedent) then Q (consequent)' as P→Q
[Lemmon]
|
|
9508
|
The sign |- may be read as 'therefore'
[Lemmon]
|
|
9512
|
We write the 'negation' of P (not-P) as ¬
[Lemmon]
|
|
9509
|
That proposition that both P and Q is their 'conjunction', written P∧Q
[Lemmon]
|
|
9510
|
That proposition that either P or Q is their 'disjunction', written P∨Q
[Lemmon]
|
|
9513
|
We write 'P if and only if Q' as P↔Q; it is also P iff Q, or (P→Q)∧(Q→P)
[Lemmon]
|
|
9514
|
If A and B are 'interderivable' from one another we may write A -||- B
[Lemmon]
|
|
9401
|
∨E: Derive C from A∨B, if C can be derived both from A and from B
[Lemmon]
|
|
9398
|
∧I: Given A and B, we may derive A∧B
[Lemmon]
|
|
9397
|
CP: Given a proof of B from A as assumption, we may derive A→B
[Lemmon]
|
|
9394
|
MPP: Given A and A→B, we may derive B
[Lemmon]
|
|
9402
|
RAA: If assuming A will prove B∧¬B, then derive ¬A
[Lemmon]
|
|
9395
|
MTT: Given ¬B and A→B, we derive ¬A
[Lemmon]
|
|
9400
|
∨I: Given either A or B separately, we may derive A∨B
[Lemmon]
|
|
9396
|
DN: Given A, we may derive ¬¬A
[Lemmon]
|
|
9393
|
A: we may assume any proposition at any stage
[Lemmon]
|
|
9399
|
∧E: Given A∧B, we may derive either A or B separately
[Lemmon]
|
|
9517
|
The 'scope' of a connective is the connective, the linked formulae, and the brackets
[Lemmon]
|
|
9516
|
A 'well-formed formula' follows the rules for variables, ¬, →, ∧, ∨, and ↔
[Lemmon]
|
|
9521
|
'Modus tollendo ponens' (MTP) says ¬P, P ∨ Q |- Q
[Lemmon]
|
|
9522
|
'Modus ponendo tollens' (MPT) says P, ¬(P ∧ Q) |- ¬Q
[Lemmon]
|
|
9525
|
We can change conditionals into negated conjunctions with P→Q -||- ¬(P ∧ ¬Q)
[Lemmon]
|
|
9524
|
We can change conditionals into disjunctions with P→Q -||- ¬P ∨ Q
[Lemmon]
|
|
9523
|
De Morgan's Laws make negated conjunctions/disjunctions into non-negated disjunctions/conjunctions
[Lemmon]
|
|
9527
|
The Distributive Laws can rearrange a pair of conjunctions or disjunctions
[Lemmon]
|
|
9526
|
We can change conjunctions into negated conditionals with P→Q -||- ¬(P → ¬Q)
[Lemmon]
|
|
9519
|
A 'substitution-instance' is a wff formed by consistent replacing variables with wffs
[Lemmon]
|
|
9518
|
A 'theorem' is the conclusion of a provable sequent with zero assumptions
[Lemmon]
|
|
9520
|
The paradoxes of material implication are P |- Q → P, and ¬P |- P → Q
[Lemmon]
|
|
9529
|
A wff is 'inconsistent' if all assignments to variables result in the value F
[Lemmon]
|
|
9531
|
'Contrary' propositions are never both true, so that ¬(A∧B) is a tautology
[Lemmon]
|
|
9534
|
Two propositions are 'equivalent' if they mirror one another's truth-value
[Lemmon]
|
|
9530
|
A wff is 'contingent' if produces at least one T and at least one F
[Lemmon]
|
|
9532
|
'Subcontrary' propositions are never both false, so that A∨B is a tautology
[Lemmon]
|
|
9533
|
A 'implies' B if B is true whenever A is true (so that A→B is tautologous)
[Lemmon]
|
|
9528
|
A wff is a 'tautology' if all assignments to variables result in the value T
[Lemmon]
|
|
9535
|
'Contradictory' propositions always differ in truth-value
[Lemmon]
|
|
9537
|
Truth-tables are good for showing invalidity
[Lemmon]
|
|
9536
|
If any of the nine rules of propositional logic are applied to tautologies, the result is a tautology
[Lemmon]
|
|
9539
|
Propositional logic is complete, since all of its tautologous sequents are derivable
[Lemmon]
|
|
9538
|
A truth-table test is entirely mechanical, but this won't work for more complex logic
[Lemmon]
|
|
13909
|
Write '(∀x)(...)' to mean 'take any x: then...', and '(∃x)(...)' to mean 'there is an x such that....'
[Lemmon]
|
|
13902
|
'Gm' says m has property G, and 'Pmn' says m has relation P to n
[Lemmon]
|
|
13910
|
Our notation uses 'predicate-letters' (for 'properties'), 'variables', 'proper names', 'connectives' and 'quantifiers'
[Lemmon]
|
|
13900
|
'Some Frenchmen are generous' is rendered by (∃x)(Fx→Gx), and not with the conditional →
[Lemmon]
|
|
13905
|
If there is a finite domain and all objects have names, complex conjunctions can replace universal quantifiers
[Lemmon]
|
|
13904
|
Universal Elimination (UE) lets us infer that an object has F, from all things having F
[Lemmon]
|
|
13906
|
With finite named objects, we can generalise with &-Intro, but otherwise we need ∀-Intro
[Lemmon]
|
|
13903
|
Universal elimination if you start with the universal, introduction if you want to end with it
[Lemmon]
|
|
13908
|
UE all-to-one; UI one-to-all; EI arbitrary-to-one; EE proof-to-one
[Lemmon]
|
|
13911
|
The 'symbols' are bracket, connective, term, variable, predicate letter, reverse-E
[Lemmon]
|