4
$\begingroup$

Definitions

Let our propositional calculus be defined as follows:

Alphabet $D := \{p_i:i\in \mathbb{N}\}$.

Operators $\Omega := \Omega_0 \cup \Omega_2$ where $\Omega_0 := \{f\}$ and $\Omega_2 := \{\rightarrow\}$.

Axioms:

  • AX1: $A\rightarrow(B\rightarrow A)$
  • AX2: $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B) \rightarrow (A\rightarrow C))$
  • AX3: $((A\rightarrow f)\rightarrow f) \rightarrow A$

where $A$, $B$ and $C$ can be arbitrary formulas.

Modus ponens is the only inference rule. To be precise, a formula $A$ is a theorem (denoted $\vdash A$) if there exists a sequence of formulas $A_1, ..., A_n$ (called an inference sequence) such that $A_n=A$ and for all $i\in \{1,...,n\}$ the following holds:

  • $A_i$ is an axiom, or
  • there exists $j,k\in \{1,...,i-1\}$ such that $A_k=A_j\rightarrow A_i$.

Word and formula

A word is a nonempty and finite sequence of symbols from the set $D\cup \Omega \cup \{(,)\}$.

A word $A$ is a formula if there exists a finite sequence of words $A_1,...,A_m$ such that $A_m=A$ and for all $i \in \{1,...,m\}$ the following holds:

  • $A_i=p_n$ for some $n\in \mathbb{N}$, or
  • $A_i=f$, or
  • $A_i=(A_j\rightarrow A_k)$ for some $j,k \in \{1,...,i-1\}$.

For brevity, the outermost parentheses can be omitted, so $(A \rightarrow B)$ is the same as $A \rightarrow B$.

Problem

Show that $\not\vdash f$.

Comments

This problem seems difficult because I somehow need to prove there exists no inference sequence that would prove $\vdash f$. Intuitively, it seems that for any inference sequence $A_1,...,A_n$, the formula $A_i$ always contains at least one arrow symbol for all $i\in \{1,...,n\}$, but I cannot figure out how to prove it.

(I believe I'm not supposed to use the soundness or completeness theorems in the proof, as they are introduced much later in the lecture notes.)

$\endgroup$
6
  • $\begingroup$ Are you allowed to use soundness : every theorem of the calculus is a tautology ? $\endgroup$
    – Mauro ALLEGRANZA
    Sep 30, 2018 at 16:25
  • $\begingroup$ @MauroALLEGRANZA No, I think not because it comes much later in the lecture notes. $\endgroup$
    – Smi
    Sep 30, 2018 at 16:31
  • 2
    $\begingroup$ Well, even if you aren't supposed to cite the soundness theorem, the easiest way to prove this might be to first prove the soundness theorem and then use it. $\endgroup$
    – Eric Wofsey
    Sep 30, 2018 at 19:06
  • $\begingroup$ Hmm, okay. The proof for the soundness theorem is included in the lecture notes, though, and there's a remark in the lecture notes saying this task "is fairly difficult", so I guess a proof that avoids citing soundness theorem won't be trivial. $\endgroup$
    – Smi
    Sep 30, 2018 at 19:41
  • $\begingroup$ If we restore parentheses to the axiom schema, then one can figure out that every theorem starts with '(' and ends with ')'. f doesn't start with '(' or with ')'. That said, if you can't use soundness, I'm not sure how to go about showing that every theorem starts with '(' and ends with ')'. $\endgroup$
    – Doug Spoonwood
    Oct 1, 2018 at 5:01

2 Answers 2

Reset to default
3
$\begingroup$

Let $V(E)$ for a propositional expression $E$ be defined as:

  • $1$ if every bivalent valuation of $E$ is true
  • $0$ if any bivalent valuation of $E$ is false

given that $'f'$ valuates to false. So for example, $V(\ulcorner A \lor (A \to f) \urcorner)$ has 2 valuations: $\top \lor (\top \to \bot) = \top$ as well as $\bot \lor (\bot \to \bot) = \top$, so its valuation is $1$.

Prove that the valuation of every axiom is $1$ (keep in mind that for example, an instance of AX1 might be $(X \to Y) \to ((M \to N) \to (X \to Y))$, that is the $A$ and $B$ in the axiom are expressions not propositional variables).

Prove that modus ponens preserves positive valuations: if $A \to B$ and $A$ has positive valuations, then $B$ must have a positive valuation. Same cavaet, $A$ and $B$ are expressions not propositional variables.

Put that together to make an inductive argument that no provable expression has a valuation of $0$. Combine that with the valuation of $\ulcorner f \urcorner$.

$\endgroup$
1
  • $\begingroup$ I like this, and I think it works, but it basically proves soundness, and assigns a value to 'f'. I have to wonder if another way works better. We don't assign a value to f, and prove consistency. Then, since (f→A) is a theorem, we could deduce A. And that would contradict consistency, since A is a theorem and so is (A→f). The difficulty I have though lies in that I don't know how to prove consistency without proving or assuming soundness. $\endgroup$
    – Doug Spoonwood
    Oct 1, 2018 at 21:02
-2
$\begingroup$
  1. None of the axioms are f. So, f could only get deduced by uses of detachment (i. e. modus ponens).
  2. Every detachment of a formula has one of the following forms 1. (B→A) originating from axiom 1. 2. A originating from axiom 1. 3. ((A→B)→(A→C)) originating from axiom 2. 4. (A→C) originating from axiom 2. 5. C originating from axiom 2. 6. A originating from axiom 3.

I'll note that all of the axioms are sound, in that none of them evaluate to f for any valuation of their variables.

(B→A), ((A→B)→(A→C)), and (A→C) do not have the same form of f. So, it is not possible to derive f such that it has the form indicated by 1., 3., or 4.

Consider the possibility that f has form A originating from axiom 1, or from axiom 3. In the first case, axiom schema 1 gets instantiated as the axiom (f→(B→f)). But, then nothing could get detached, since the axioms are sound. Thus, (B→f) would not be derivable, and neither would f. So, f cannot get derived that way. In the second case, axiom schema 3 gets instantiated as the axiom (((f→f)→f)→f). But, the antecedent of that axiom is ((f→f)→f), which is false. Since the axioms are sound, that does not permit a deduction of f. Thus, both possibilities 2., and 6. consider here cannot derive f.

Finally, we come to the possibility that f got derived having form C from axiom 2. Then axiom schema 2 gets instantiated as an axiom having the form ((A→(B→f))→((A→B)→(A→f))). In order to get to f, since all of the axioms are true, and the deduction rule of modus ponens is sound, it follows that (A→(B→f)), (A→B), and A all hold true. But, if A holds true, and (A→B) holds true, so does B. Then since B is true, (B→f) is false. Since (B→f) is false, and A is true, that would imply (A→(B→f)) as false. But, that is not possible since the axioms are sound.

Having eliminated all possible cases of how f could get deduced according to the definition of a proof, we conclude that f is not provable.

$\endgroup$
6
  • $\begingroup$ Your statement (2) is wrong. For instance, if the formula $A$ itself is an implication, then you might deduce $A$ via axiom 1, and then deduce the consequent of $A$ from $A$. So, you need to rule out not just any of these formulas being $f$ themselves but also not being any nested sequence of implications whose final consequence is $f$. $\endgroup$
    – Eric Wofsey
    Sep 30, 2018 at 19:03
  • $\begingroup$ And in fact you can't rule that out, since (for instance) $f\to(p_1\to f)$ is an axiom whose final consequent is $f$. And there are more complicated formulas too like $p_1\to((p_1\to f)\to f)$ which are theorems and have $f$ as a final consequent. So, I am skeptical that any simple syntactic analysis like this can work. $\endgroup$
    – Eric Wofsey
    Sep 30, 2018 at 19:11
  • $\begingroup$ In any case, if you are going to use the fact that the axioms are true for all valuations and that modus ponens is sound, there is of course a much easier proof which is just to observe that $f$ is not true for all valuations. $\endgroup$
    – Eric Wofsey
    Sep 30, 2018 at 19:22
  • $\begingroup$ @EricWofsey I think the nested sequence of implications gets covered by cases 2., 4., and 5. "since (for instance) f→(p1→f) is an axiom whose final consequent is f." f is not an instance of axiom, and thus there is no valid way to use the formula (f→(p1→f)) in any detachment. So, (p1→f) cannot get derived, nor can f from that axiom. "(p1→((p1→f)→f))" sure, but so what? p1, effectively being a propositional constant, is not an axiom. So, you can't derive anything from that. $\endgroup$
    – Doug Spoonwood
    Sep 30, 2018 at 19:26
  • $\begingroup$ But it is extremely non-obvious that something like that must be the case for every nested sequence of implications ending in $f$ which is a theorem. (For one thing, you have not actually proved that $p_1$ is not a theorem. Of course this follows from soundness, but if you're going to use soundness then the problem itself is immediately trivial.) $\endgroup$
    – Eric Wofsey
    Sep 30, 2018 at 19:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .