CPL - Classical Predicate Logic

CPL is the standard bivalent logic with values T and F.


Semantics

Truth Values

Common labels for the values include:

T

1

true

F

0

false

Truth Tables

The value of a sentence with a truth-functional operator is determined by the values of its operands according to the following tables.

Negation
¬
T F
F T
Conjunction
∧ T F
T T F
F F F
Disjunction
∨ T F
T T T
F T F

Defined Operators

The Material Conditional ⊃ is definable in terms of disjunction:

A ⊃ B \(:=\) ¬A ∨ B

Likewise the Material Biconditional ≡ is defined in terms of ⊃ and ∧:

A ≡ B \(:=\) (A ⊃ B) ∧ (B ⊃ A)
Material Conditional
⊃ T F
T T F
F T T
Material Biconditional
≡ T F
T T F
F F T

Compatibility Tables

CPL does not have separate Assertion or Conditional operators, but we include tables and rules for them, for cross-compatibility.

Assertion
⚬
T T
F F
Conditional
→ T F
T T F
F T T
Biconditional
↔ T F
T T F
F F T

Predication

The value of predicated sentences are handled in terms of a predicate's extension.

A sentence with n-ary predicate \(P\) over parameters \(\langle a_0, ... ,a_n\rangle\) has the value T iff \(\langle a_0, ... ,a_n\rangle\) is in the extension of \(P\).

Note

CPL does not give a treatment of the quantifiers. Quantified sentences are treated as opaque (uninterpreted). See CFOL for quantification.

Consequence

Logical Consequence is defined as follows:

Logical Consequence

C is a Logical Consequence of A iff all models where the value of A is T are models where C also has the value T.

Tableaux

Nodes

Each node consists of a sentence.

Trunk

To build the trunk for an argument, add a node for each premise, and a node with the negation of the conclusion.

To build the trunk for the argument A1 ... An ∴ B write:
A1
⋮
An
¬B

Closure

⊗Contradiction Closure[source]
A
⋮
¬A
⊗
⊗¬=Self Identity Closure[source]
⋮
a ≠ a
⊗
⊗¬E!Non Existence Closure[source]
⋮
¬E!a
⊗

Rules

In general, rules for connectives consist of two rules per connective: a plain rule, and a negated rule. The special case of negation only one rule for double negation.

There is also a special rule for the Identity predicate.

Operator Rules

¬ Rules
¬¬KDouble Negation[source]
¬¬A
⋮
A
∧ Rules
∧KConjunction[source]
A ∧ B
⋮
A
B
¬∧KConjunction Negated[source]
¬(A ∧ B)
⋮
¬A
¬B
∨ Rules
∨KDisjunction[source]
A ∨ B
⋮
A
B
¬∨KDisjunction Negated[source]
¬(A ∨ B)
⋮
¬A
¬B
⊃ Rules
⊃KMaterial Conditional[source]
A ⊃ B
⋮
¬A
B
¬⊃KMaterial Conditional Negated[source]
¬(A ⊃ B)
⋮
A
¬B
≡ Rules
≡KMaterial Biconditional[source]
A ≡ B
⋮
¬A
¬B
B
A
¬≡KMaterial Biconditional Negated[source]
¬(A ≡ B)
⋮
A
¬B
¬A
B

Compatibility Rules

⚬ Rules
⚬KAssertion[source]
⚬A
⋮
A
¬⚬KAssertion Negated[source]
¬⚬A
⋮
¬A
→ Rules
→KConditional[source]
A → B
⋮
¬A
B
¬→KConditional Negated[source]
¬(A → B)
⋮
A
¬B
↔ Rules
↔KBiconditional[source]
A ↔ B
⋮
¬A
¬B
B
A
¬↔KBiconditional Negated[source]
¬(A ↔ B)
⋮
A
¬B
¬A
B

Notes

References