Propositional Logic as a Calculus Flashcards
1. Natural Deduction Calculus 2. Axiomatic Calculus 3. GEB Calculus
When is an inference valid?
Whenever it is impossible for the premises to be true and the conclusion to be false, the inference is valid
What are two ways propositional logic is used?
- Express complex statements (trees)
- Conclude or infer certain statements from others (calculus)
Is entailment semantic or syntactic
Semantic
What is the notion of validity?
Semantic notion, since it refers to the meaning of wffs - in terms of its truth values.
Can be used to define when a wff A (conclusion) follows from the set of wffs (premises):
A wff A is a (semantic) consequence of a set of wffs A0, …, An (or A0, …, An entails A) if it is impossible that A0, …, An are all true and A is false at the same time. Write as:
A0, …, An ⊨ A
How can wffs be defined as a notion of validity?
A wff A is a (semantic) consequence of a set of wffs A0, …, An (or A0, …, An entails A) if it is impossible that A0, …, An are all true and A is false at the same time. Write as:
A0, …, An ⊨ A
How to know if the premises are true and the conclusion is false?
Try all the possible truth assignment values. Find the row were all the premises are true then look at the conclusion.
A0, …, An ⊨ A
T ⊨ F
Therefore, must be decidable and have a decision prodecure
What happens when the conclusion A in entailment (A0, …, An ⊨ A) is always true regardsless of the truth value assignment?
Then, it is a semantic consequence of the empty set, just written as ⊨ A
What is the difference between entailment and implication?
Truth Conditions Similar
Entialment: (⊨)
* Meta-langugae (How formulas relate to other formulas)
* Different kind of truth: taking about relation
* Semantic
Implication: (⊃)
* Formulas (language) and Object language: (Formula. Ex: (A ∧ B))
* Bivalence (true or false)
* Syntax
Natural Deduction Calculus
What is natural deduction calculus?
System allows to do proofs for natural logic + inference rules
Inference rules: written with premises above the horizontal line and a conlcusion below it
Read from top to bottom: formally deduce the conclusion from the premises.
Sets of formulas connected by inference rules
Natural Deduction Calculus
Modus Ponens:
That B follows from A ⊃ B expressed as a syntactic rule of inference: MODUS PONENS
Read from top to bottom: formally deduce the conclusion
Natural Deduction Calculus
What are the rules for conjuction
And-elimination and And-introduction
Allows the elimination of a conjuction symbol, thus “∧-Elim”.
Alternative, introduce a conjuction symbol, we need both A and B as premises.
Natural Deduction Calculus
Define a derivation or proof in NDC?
By applying one+ inference rules we obtain a derivation or proof in the form of a tree.
Natural Deduction Calculus
Natural Deduction Proof 1:
(A ∧ B ⊢ B ∧ A)
Meaning “⊢”:
Symbol for LOGICAL THEOREMS:
Means that Q is derivable from P in the system. Consistent with its use for derivability, a “⊢” followed by an expression without anything preceding it denotes a theorem, which is to say that the expression can be derived from the rules using an empty set of axioms.
Natural Deduction Calculus
How to write the conclusion of the tree in NDC?
Formulas top of a derivation tree are the premises (used multiple times in a derivation) and the conclusion is at the bottom of the tree.
If A is obtained by a derivation from the premises A0, …, An, we have:
A0, …, An ⊢ A
Natural Deduction Calculus
What is Implication Elimination?
Modus ponens eliminates an implication formula: “⊃-Elim”
Is (A ∧ B) and (B ∧ A) logically equivalent?
(A ∧ B) ≠ (B ∧ A)
Different formulas so not logically equivalent
Natural Deduction Calculus
Implication introduction:
Allows us to infer A ⊃ B, from a proof B from the assumption A.
* Original assumption of A becomes internalized in colcusion so it is dischanged from proof (expressed by square brackets around assumption [A])
* Discharged assumption does not count as an assumption in the proof and cannot be used fruther down the proof tree.
Open Assumptions: Assumptions that are not dischanged
Appying “⊃-Intro” rule to derivation in proof 1, both occurances of the assumption dischanged because they both appear above the formula tree.
Natural Deduction Calculus
What are open and closed assumptions?
Allows us to infer A ⊃ B, from a proof B from the assumption A.
* Original assumption of A becomes internalized in colcusion so it is dischanged from proof (expressed by square brackets around assumption [A])
* Discharged assumption does not count as an assumption in the proof and cannot be used fruther down the proof tree.
Open Assumptions: Assumptions that are not dischanged
Natural Deduction Calculus
What is the special case for implication elimination?
If “B” is true, then A= irrelevent.
Preserves truth
Natural Deduction Calculus
Derive A ⊃ (B ⊃ A) with no open assumptions:
What is logical theorem?
Only derived from logic, not other theorems
Formulas like A ⊃(A ⊃ B) which can only be proved in derivations without open assumptions are called logical theorems.
Use symbol (⊢)
Natural Deduction Calculus
Introduction Rules for Disjunction:
Natural Deduction Calculus
Elimination Rule for disjunction:
This is a structure for proof by cases
Natural Deduction Calculus
Formula for introduction and elimination rules for negation:
Symbol: “⊥” (propostion tha is always false - a contradiction)
Natural Deduction Calculus
Is a (A) = (~~ A)
Not the same formula (syntax)
Though they are logically equivalent (semantics)
In the GEB system, the “~~ “ can be cancelled out
Natural Deduction Calculus
Derive B ∨ D from the assumptions A V C, A ⊃ B, and C ⊃ D.
Argument form of ‘dilemma’
Proof 3:
Natural Deduction Calculus
Prove:
A V ~ A (tertium non datur; law of the excluded middle) is a theorem.
Proof 4:
Axiomatic Calculus
What is Axiomatic Calculus?
Proof system
Good system - only one rule (modus ponens) and axioms
- Inference Rule: From A and A ⊃ B infer B (modus ponens)
- Substitution Rule: Any wff can be substitued for the metalofical variables A, B, and C
Natural Deduction calculus has many rules of inference
Define proof (for calculus):
Sequence of formulas (wff axioms / obtained through inference rules)
Axiomatic Calculus
Why is it called “axiomatic”?
it consists of following 10 axiom schemata which can serve as a starting points for derivations
Axiomatic Calculus
How does the system allow for a concise recursive definition of proofs?
A proof of a wff A from a sets of assumptions A0, …, An is a sequence of wffs, such that each of them is either
a) an assumption, or
b) an instantiation (the result of applying a substitution) of one of the axiom schemata, or
c) obtained from a previous wffs in the sequence by modus ponens
Axiomatic Calculus
Show: A ⊃ A ⊢B ⊃ (A ⊃ A)
Axiomatic Calculus
Show: A ⊃ B, B ⊃ C ⊢ A ⊃ C
Proof 3:
Axiomatic Calculus
Show: ⊢ (A ∧ ~ A) ⊃ B
Proof #4
GEB System
Joining and Separation Rule
GEB System
Double-tilde Rule:
The string ‘~~ ‘ can be deleted from any theorem. Also inserted into any theorem
GEB System
Fantasy Rule:
If B can be derived when A is assumed in a theorem, then (A ⊃ B) is a theorem
⊃-Introduction
GEB system
Carry-over Rule:
Inside a fantasy, any theorem from reality one level higher can be brought in and used
GEB system
Rule of Detachment:
If A and (A ⊃ B) are theorems, then B is a theorem
GEB System
Contrapositive Rule, De Morgan’s Rule, and Switcheroo Rule
GEB System
Proof 1: (A ∧ B) ⊃ (B ∧ A)
What are the semantic and syntactical notions of consequence?
What is meta-logic?
Used when systems are isomorphic (such as the different calculus systems)
What are the equivalence of proof systems?
System of Natural deduction, axiomatic proof system, and GEB systems prove the same theorems
How to show the equivalence of ND with axiomatic calculus:
a. Use the ND system to derive all the axioms of the axiomatic system
b. Use the axiomatic system to justify all the rules of the ND system.
What is the relation between the semantic method of proof and the syntactic one?
Natural Deduction Calculus
(P → R) ∧ (Q → R) ⊢ (P ∨ Q) → R
Natural Deduction Calculus
(P ∧ Q) → R ⊢ P → (Q → R)
Natural Deduction Calculus
P ∧ Q → Q ∧ P
Natural Deduction Calculus
P ∧ Q → Q ∧ P
Natural Deduction Calculus
P → Q, Q → R ⊢ P → R
Natural Deduction Calculus
P ∧ Q, P → R, Q → S ⊢ R ∧ S
Natural Deduction Calculus
P ∨ Q, ~Q ⊢ P
Natural Deduction Calculus
~P → P ⊃ Q
Homework 03:
Show that B V (A ⊃ A) is a tautology
Homework 03:
Prove B V (A ⊃ A) through Natural Deduction Calculus
Homework 03:
Prove B V (A ⊃ A) using the axiomatic calculus:
Homework 03:
Prove B V (A ⊃ A) using the GEB calculus:
Homework 03 - Handout 2b, Exercise 8
P1, P2 |= ∼P1 ⊃ P2) ⊃ (P2 ⊃ P1)?
Homework 03 - Handout 2b, Exercise 10
Answer the question:
Homework 03 - Handout 2b, Exercise 15
A proof of P ⊃ (Q ⊃ (P ∧ Q)) in Natural Deduction:
Homework 03
Explain formal language:
To explain these ideas to a friend, you first need to tell them that we’re discussing a formal language called Propositional Logic. This formal language, as opposed to a natural language like English, is designed to represent and reason about basic logical reasoning. We define our language in two parts: Firstly, with a vocabulary (alphabet) and a grammar (the syntax), and secondly with an unambiguous interpretation (semantics) of its grammatical sentences (well-formed formulas). You should also point out that the grammar of this language has a very simple (recursive) structure.
Homework 03:
Difference between semantic entailment and provability:
The difference between semantic entailment ( |=) and provability ( ⊢). Both notions describe a relationship of consequence between a set of premises (Γ) and a conclusion A, but semantic entailment corresponds to the interpretation of consequence in Propositional Logic, whereas provability corresponds to a method that establishes consequence in Propositional Logic on the basis of sentence structure. If we say that Γ entails A, we mean that A is a consequence of Γ according to the unique interpretation that is part of the language of Propositional Logic, whereas if we say that Γ proves A, we mean that a method that examines the structure of the sentences in Γ and A tells us that A is a consequence of Γ.
Homework 03
What it means for Propositional Logic to be sound
What it means for Propositional Logic to be sound.
If whenever the provability test says “Yes” the entailment test says “Yes” then Propositional Logic is sound. This means that the method that examines the structure of Γ and A only tells us that there is a logical consequence between A and Γ if there really is one according to the interpretation of Propositional Logic. However, it is possible that the method will reject some Γ, A (i. e., respond with a “No”) even though A is a consequence of Γ according to the interpretation given to Propositional Logic. In other words, soundness tells us that the syntactic method identifies only those consequence relationships that agree with PL semantics, but not necessarily all of them.
So the fact that propositional logic is both sound and complete means that, given a set of premises Γ and a conclusion A, the result of a Natural Deduction (or axiomatic) derivation Γ ` A and the result of a truth table test for Γ |= A are always in agreement.
In other words, the semantic and syntactic notions of consequence are equivalent, and we can thus use one or the other interchangeably
Homework 03
What it means for Propositional Logic to be complete
What it means for Propositional Logic to be complete.
Completeness is the opposite relationship. It tells us that the syntactic method identifies all of the consequence relationships that agree with PL semantics, but it might also pick out some bad ones, too. Put another way, if whenever our entailment test says “Yes” the provability test says “Yes” then Propositional Logic is complete. However, it is possible that the provability test will say “Yes” to some Γ and A whereas the entailment test will reject Γ and A.
So the fact that propositional logic is both sound and complete means that, given a set of premises Γ and a conclusion A, the result of a Natural Deduction (or axiomatic) derivation Γ ` A and the result of a truth table test for Γ |= A are always in agreement.
In other words, the semantic and syntactic notions of consequence are equivalent, and we can thus use one or the other interchangeably
P → Q , Q → R ⊢ P → (Q ∧ R)
