1
$\begingroup$

I want to prove the soundness of propositional logic without using induction. I think I can do that via a process that's basically universal introduction (i.e., demonstrate something about an arbitrary member and infer that it applies universally). As an example of this approach I've picked a new inference rule to prove.

My questions:

  • Is my approach valid?
  • Is my proof correct?
  • Is it easy to understand and follow?
  • Do I need to add more/less detail?
  • How else can I improve it?

Proof

We want to show that $\boxed{\dfrac{\Gamma_1 ,\,\phi\vdash\psi\quad\Gamma_2,\,\lnot\phi\vdash\psi}{\Gamma_1 ,\,\Gamma_2\vdash\psi}}\def\pa {((\Gamma_1\land\phi)\longrightarrow\psi)} \def\pb {((\Gamma_2\land\lnot\phi)\longrightarrow\psi)} \def\ca {((\Gamma_1\land\Gamma_2)\longrightarrow\psi)} \def\lto {\longrightarrow} \def\val#1{V_\mathscr{I}( #1 )} \def\pli {\text{PL-interpretation, $ $\mathscr{I}$},} \def\inp{\mathscr{I}}$ is a truth preserving inference rule without using induction. To do so we'll convert the rule to an axiom schema and show that it's valid.

Conversion Rules

Symbols
  • "," and the "$\quad$" convert to conjunction
  • "$\vdash$" and the vinculum convert to implication
  • $\Gamma$, with or without subscript, is a finite set of conjoined wffs, so it's simply a wff with it's own valuation rules
Valuation of $\Gamma$
  • $\val{\Gamma}=1$ iff, for all $\gamma\in\Gamma$, it's the case that $\val{\gamma}=1$ and $\Gamma\neq\emptyset$

Conversion

  • $\Gamma_1 ,\,\phi\vdash\psi:= \pa$

  • $\Gamma_2,\,\lnot\phi\vdash\psi:= \pb$

  • $\Gamma_1 ,\,\Gamma_2\vdash\psi:= \ca$

  • Putting it all together, the rule converts to - $\boxed{((\pa\land\pb)\lto\ca)}$

Proof that the axiom schema is valid

  1. Assume for reductio that $\val {((\pa\land\pb)\lto\ca)}=0$

  2. It follows from (1) that $\val {\ca}=0$

  3. It follows from (2) that $\val{\Gamma_1}=1$, $\val{\Gamma_2}=1$, and $\val{\psi}=0$

  4. It follows from (1) that $\val{\pa}=1$

  5. It follows from (3) and (4) that $\val{\phi}=0$

  6. It follows from (5) that $\val{\lnot\phi}=1$

  7. It follows from (1) that $\val{\pb}=1$

  8. It follows from (3) and (6) that $\val{\pb}=0$, which contradicts (7) $\boxed{}$

Example Proof

$\begin{array}{lrcll} 1.&\phi&\vdash &\phi &\text{RA}\\ 2.&\phi&\vdash &\lnot\psi\lor\phi &\text{1, $\lor$I}\\ 3.&\phi&\vdash &\psi\to\phi &\text{2, Abbrv}\\ 4.&\phi&\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{3, $\lor$ I}\\ 5.&\lnot\phi&\vdash &\lnot\phi &\text{RA}\\ 6.&\lnot\phi&\vdash &\lnot\phi\lor\psi &\text{5, $\lor$I}\\ 7.&\lnot\phi&\vdash &\phi\to\psi &\text{6, Abbrv}\\ 8.&\lnot\phi&\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{7, $\lor$ I}\\ 9.&\emptyset &\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{4, 8 New Rule}\\ \end{array}$

$\endgroup$
10
  • $\begingroup$ ... provided that $\Gamma_i$ are finite sets of formulas, otherwise $\Gamma_i \land \phi$ is not a formula. $\endgroup$ Sep 10 '21 at 10:00
  • $\begingroup$ @Mauro ALLEGRANZA, I've explicitly mentioned that $\Gamma$ is a finite set, but I could draw further attention to it if it makes things clearer? $\endgroup$
    – Ten O'Four
    Sep 10 '21 at 10:07
  • $\begingroup$ But this is the key-point: if the number of cases is finite, we do not need induction. It is enough to check them one-by-one. $\endgroup$ Sep 10 '21 at 10:09
  • $\begingroup$ @Mauro ALLEGRANZA, while each substitution instance is composed of a finite number of wffs, there are an infinite number of substitution instances, though $\endgroup$
    – Ten O'Four
    Sep 10 '21 at 10:18
  • $\begingroup$ To prove your concerned sentential soundness theorem, normally we need to use RAA to prove each logical connective's soundness case by case. Since each connective has different meaning, what's the most important principle upon which you can claim your single universal inference rule can ensure each row of the truth table of every connective to acting exactly according to their respective definition? The famous XOR connective, for example, has a very peculiar elimination rule, how your proposed theory can ensure it's not acting like the usual wrong elimination rule mimic disjunction syllogism? $\endgroup$
    – mohottnad
    Sep 10 '21 at 23:35
2
$\begingroup$

It's easier to use Heyting algebra lattice model to understand the usual induction proof on the height of derivations of soundness in both intuitionistic and classical logic. And every Boolean algebra is a Heyting algebra which is also distributive.

In mathematics, a Heyting algebra (also known as pseudo-Boolean algebra) is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b of implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b).

In the link there's a lattice diagram, every natural deduction rule of each connective can be checked to preserve the order of such lattice according to the lattice formation definitions. But you still need to climb up the lattice for an arbitrary derivation with finite steps. But this height in the lattice doesn't correspond to the entities or terms of the domain of discourse of such a structure, so you cannot invoke "universal introduction" as a natural deduction inference rule. Back in territory with your valuation function, this height complexity corresponds to the individual step of your proof which is not an entity of its domain of discourse (thus no universal introduction applicable here), so induction seems necessary here.

$\endgroup$
4
  • $\begingroup$ Thanks for that, I'll have a play 😊 The inference rule I've chosen is actually quite handy in proving theorems. Something is a theorem if it contains some wff disjoined with it's negation. As such a theorem can be constructed from both it's wff and it's negation through disjunction intro. Realising that allows us to avoid annoyances, like multiple applications of RAA, and makes the proof shorter and more readable. Though it would be very unwieldy, I think it can actually prove every theorem in PL $\endgroup$
    – Ten O'Four
    Sep 13 '21 at 7:06
  • $\begingroup$ I'm getting my head round this a bit. There are no steps in my translated proof system, though? All there is is axiom schema and substitution, which, incidentally, every standard proof of soundness takes as a given. For a standard hilbert style the base case is showing the axiom schema are valid, exactly like I've done, and the inductive step, which relies on substitution to show all instances that MP can be applied, is valid - we're done with the axiom schema. A proof in my system is basically just unweildly function composition. It's UI on wffs that can be substituted $\endgroup$
    – Ten O'Four
    Sep 13 '21 at 15:44
  • $\begingroup$ @TenO'Four thx for your elaboration of your substitution schema. You can certainly call your version as some kind of "recursion" or "induction" on wffs that can be substituted. In logic UI is strictly ranging over variables of domain, not wffs. Sorry I still don't fully understand your special sequent calculus structural rule (your favored negated disjunction, is there a name for it?), let alone converted to axiom schema, but seems make sense to me. Imagine a proof assistant robot does your job to prove soundness for an arbitrary formula, I feel recursion is still needed in Hilbert system. $\endgroup$
    – mohottnad
    Sep 14 '21 at 4:45
  • $\begingroup$ Metavariables take wffs as their input, though? Either way, I think substitution needs proved, and it could well be that I've moved things from "length of proof" to "length of string". The overall idea for this is a scheme that I can translate languages into, mechanically prove soundness there, then, by virtue of equivalence, have proved soundness in the original language. What you've shared has been very helpful, thanks 😊 I've edited in an example proof using the rule. It doesn't have a name, but I think "theorem checker" sums up what it does. $\endgroup$
    – Ten O'Four
    Sep 14 '21 at 5:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.