2

The problem is based on Tomassi's Logic - Exercise 6.3 Question 10 (1). The object is to prove $\forall x[Fx \to Gx] : \exists x[Fx] \to \exists y[Gy]$ in 7 lines. All deductive apparatus is allowed except EE or any Passing Rules (can do the proof in 8 lines using a Passing Rule). As far as SI and TI goes, no problem in the book has required their use so far, so I suspect that they aren't required, but they aren't prohibited. I've included the shortest proof I've found so far, but I'm really stumped on how to get it down to 7 lines. Any help would be greatly appreciated.

$\begin{array}{llll}&\{1\} &1. &\forall x[Fx \to Gx] &\small\text{P}\\ &\{2\} &2. &\lnot (\exists x[Fx] \to \exists y[Gy]) &\small\text{A for RAA}\\ &\{2\} &3. &\exists x[Fx] \land \lnot \exists y [Gy] &\small\text{SI 2}\\ &\{4\} &4. &Fa &\small\text{A for RAA}\\ &\{1\} &5. &Fa \to Ga &\small\text{UE 1}\\ &\{1, 4\} &6. &Ga &\small\text{MP 4, 5}\\ &\{1, 4\} &7. &\exists y[Gy] &\small\text{EI 6}\\ &\{2\} &8. &\lnot \exists y[Gy] &\small\text{$\land$E 3}\\ &\{1, 2, 4\} &9. &\exists y[Gy] \land \exists \lnot y[Gy] &\small\text{$\land$I 7, 8}\\ &\{1, 2\} &10. &\lnot Fa &\small\text{RAA (4), 9}\\ &\{1, 2\} &11. &\forall x[\lnot Fx] &\small\text{UI 10}\\ &\{1, 2\} &12. &\lnot \exists x[Fx] &\small\text{SI 11}\\ &\{2\} &13. &\exists x[Fx] &\small\text{$\land$E 3}\\ &\{1, 2\} &14. &\exists x[Fx] \land \lnot \exists x[Fx] &\small\text{$\land$I 12, 13}\\ &\{1\} &15. &\lnot \lnot (\exists x[Fx] \to \exists y[Gy]) &\small\text{RAA (2), 14}\\ &\{1\} &16. &\exists x[Fx] \to \exists y[Gy] &\small\text{DNE 15}\\ \end{array}$

(1) Tomassi's actual question is $\forall y[Gy \to Hy] : \exists x[Gx] \to \exists y[Hy]$. I've no idea why my brain decided to edit it, but, as there's no interpretation, it makes no difference to the proof.

Edit: Here's the proof using a passing rule. As this hasn't even been mentioned in the book, it's highly unlikely that this is the solution :(

$\begin{array}{llll}&\{1\} &1. &\forall x[Fx \to Gx] &\small\text{P}\\ &\{2\} &2. &Fa &\small\text{A for CP}\\ &\{1\} &3. &Fa \to Ga &\small\text{UE 1}\\ &\{1, 2\} &4. &Ga &\small\text{MP 2,3}\\ &\{1, 2\} &5. &\exists y[Gy] &\small\text{EI 4}\\ &\{1\} &6. &Fa \to \exists y[Gy] &\small\text{CP (2), 5}\\ &\{1\} &7. &\forall x[Fx \to \exists y[Gy]] &\small\text{UI 6}\\ &\{1\} &8. &\exists x[Fx] \to \exists y[Gy] &\small\text{SI 7 (passing rule)}\\ \end{array}$

Ten O'Four
  • 1,056
  • Which rules are you allowed to use to eliminate $\exists$ and to introduce $\to$? – Taroccoesbrocco Jun 13 '21 at 06:42
  • Existential Elimination isn't allowed at all, the point of the exercise, as far as the book is concerned, is to show the power of Existential Intro. As for the conditional, just a conditional proof, though I might be misunderstanding you. – Ten O'Four Jun 13 '21 at 06:52
  • 1
    I've heard of code golf, but not this is the first time I've seen formal logic golf.... – Alan Jun 13 '21 at 06:53
  • So I found this version of the book but I can't find your exercise. Am I looking at a different edition than yours? – Léreau Jun 13 '21 at 06:59
  • 1
    @Lereau that looks right. I just checked and he uses $\forall y[Gy \to Hy]: \exists x[Gx] \to \exists y[Hy]$, which doesn't make a difference for the proof, but it clearly made a diff for looking it up! No idea why my brain decided to edit it – Ten O'Four Jun 13 '21 at 07:59
  • @TenO'Four Oh wait. No what I was actually missing was where the number of lines you were referring to came from. I only now realized that this is probably indicated by the $(7)$ at the end of the line. – Léreau Jun 13 '21 at 08:24
  • Could you list the axioms and the inference rules? Or say if there is a place in this book where all of them are presented? – Maxim Nikitin Jun 13 '21 at 08:25
  • At the first blush the shorter way is a kind of $\forall x(Fx\rightarrow Gx),(Fa\rightarrow Ga),Ga\rightarrow\exists yGy,Fa\rightarrow\exists yGy,\exists xFx\rightarrow\exists yGy$. But I'm not sure about your certain calculus. – Maxim Nikitin Jun 13 '21 at 08:29
  • @Lereau, that's it :) No answers, just how many lines he took to solve it; it's very frustrating sometimes. – Ten O'Four Jun 13 '21 at 08:30
  • @MaximNikitin, there are no axioms in play, and the inference rules are everything in classical propositional logic, and UI, UE, and EI from classical Quantificational logic with identity. As far as sequents and theorems go, all major derived rules have been proved so are useable (stuff like DeM, Disjunctive Syll, all equivalences required for truth tree proofs, etc.), but I suspect aren't needed. Put another way, the only thing you can't use is existential elimination or any passing rules (unless you prove it within the proof, because it hasn't been proved yet). – Ten O'Four Jun 13 '21 at 08:40
  • @MaximNikitin, I'm not following what you're doing with that last line, could you put up an answer please so I can see? – Ten O'Four Jun 13 '21 at 08:51
  • 1
    Maybe it is only a typo... See later, the proof with EE: it has 7 steps. – Mauro ALLEGRANZA Jun 13 '21 at 12:59
  • 1
    @MauroALLEGRANZA, I really hope not :( I've been messing with this for a few days now. That does spark an idea, though. Let's say the proof, without EE, has to be done using RAA, but EE allows a direct proof. Let's also say that even with EE there exist proofs that need RAA - does that mean we're missing deductive apparatus? I'm not talking about completeness here, I'm talking about style of syntactic proofs. – Ten O'Four Jun 13 '21 at 13:44
  • What do you mean precisely by "passing rules"? Can you list them? What are the rules SI and TI you mentioned in the OP? – Taroccoesbrocco Jun 15 '21 at 05:47
  • If you look at the other comment section there's a link to the passing rules, and I've edited in another proof using the appropriate one in my question. SI and TI are sequent intro and theorem intro. – Ten O'Four Jun 15 '21 at 10:28

1 Answers1

1

I am not sure that all of the rules I used are 'legal' in your case. That's more like a Hilbert-style proof. I hope it could be useful for you.

  1. $\forall x[Fx\rightarrow Gx];$

Using $\cfrac{\forall xAx}{Ay}$ we gain

  1. $Fx\rightarrow Gx;$

Line 3 was probably proved by you before.

  1. $Gx\rightarrow\exists yGy;$

From lines 2 and 3 using syllogism $\cfrac{A\rightarrow B;\quad B\rightarrow C}{A\rightarrow C}$ we obtain

  1. $Fx\rightarrow\exists yGy;$

The final step is the application of $\cfrac{Ax\rightarrow B}{\exists xAx\rightarrow B}$. It is permited sinse $x$ is not a free variable in $B=\exists yGy$. So, we get

  1. $\exists xFx\rightarrow\exists yGy.$
Maxim Nikitin
  • 1,323
  • 1
    I see what you're doing. The last line is an application of a passing rule. Basically, from $Fa \to \exists y[Gy]$ we can apply universal introduction, giving $\forall x[Fx \to \exists y[Gy]]$ and then the passing rule to give the conclusion (we can do it 1 step using SI). Here's the rule - https://logic-text.eu/3.7.LogicalTransformationInPL.html - It can be applied here because UI can be applied, if the premise was $Fa \to \exists y[Gy]$ it wouldn't be valid. The problem is that it hasn't been covered yet so I can't see how that would be the solution :( – Ten O'Four Jun 13 '21 at 09:26
  • Unfortunately, I am not that familiar with natural deduction yet. All I can produce are Gentzen and Hilbert style proofs... Sorry. : ( – Maxim Nikitin Jun 13 '21 at 09:53
  • no sorry required :) You basically went where I did with my proof using the passing rule. What I'll do is I'll add that proof to my question so you can get a look. – Ten O'Four Jun 13 '21 at 10:20