Skip to main content
109 votes
Accepted

"Modus moron" rule of inference?

It's true that if $P$ is false then $P\Rightarrow Q$ is true. But the question is not asking if $P\Rightarrow Q$ is true, it's asking you if you can infer $P$ from $P\Rightarrow Q$ and $Q$. Let's be ...
anon's user avatar
  • 152k
63 votes
Accepted

Does every proof need an axiom saying it works?

This is a complicated question to answer for multiple reasons. We really have to say something about the foundational crisis to give a full account of the story here. Here is a caricatured brief ...
Qiaochu Yuan's user avatar
59 votes

"Modus moron" rule of inference?

This pattern is a logical fallacy called Affirming the Consequent, though I often call it Modus Bogus. To show it is not a valid inference, here is a simple Refutation by Logical Analogy: If I have ...
Bram28's user avatar
  • 101k
32 votes

"Modus moron" rule of inference?

Even if affirming the consequent is not valid, other logical rules still work. Other logical rules still work. Therefore, affirming the consequent is not valid?
Davislor's user avatar
  • 2,596
20 votes

"Modus moron" rule of inference?

Not stated in the other answers so far is that you misunderstood the meaning of logical validity, which means that, in every situation where the premises hold, the conclusion also holds. Now you may ...
user21820's user avatar
  • 59.1k
16 votes

Why not ban nested quantifiers over the same variable?

It could be done, as described in the other answers. But it would not make capture-avoiding substitution easier to define, so there's no real benefit. On the other hand, we would lose the sometimes ...
hmakholm left over Monica's user avatar
13 votes

"Modus moron" rule of inference?

As others have said, the question is asking whether it is necessarily the case that whenever $P \Rightarrow Q$ and $Q$ are true, $P$ must be true. My personal favoured instantiations of $P$ and $Q$ ...
dbmag9's user avatar
  • 980
13 votes

Why not ban nested quantifiers over the same variable?

The issue is that that kind of rule requires awareness of the contents of smaller wffs. Think about the other rules - none of them say anything about "if such-and-such a symbol appears inside...". The ...
Reese Johnston's user avatar
11 votes

"Modus moron" rule of inference?

if P⇒Q and Q it does not matter whether P or ¬P That's the point. It doesn't matter whether $P$ or $\neg P$: The statement becomes true for $P$ and $\neg P$ either. Therefore, you can not deduce ...
Natalie Clarius's user avatar
10 votes

"Modus moron" rule of inference?

The other answers have perfectly settled this question, however I thought I would share another funny example. It is not exactly the same logical structure, but very similar. This example originates ...
Eff's user avatar
  • 13.1k
10 votes
Accepted

Converse of Deduction Theorem

Yes, it is just a quick consequence of the elimination rule. $\to $ Elimination (in its most common phrasing) says that if $\Gamma\vdash A\to B$ and $\Gamma\vdash A$ then $\Gamma\vdash B.$ So, if $\...
spaceisdarkgreen's user avatar
10 votes
Accepted

Are there axioms in a natural deduction system?

Hilbert system and natural deduction can be seen as two "dual" approaches to writing formal proofs. Roughly, when it comes to deriving formulas that are valid in a specific logical system (...
Taroccoesbrocco's user avatar
9 votes

Proving 'Law of Excluded Middle' in Fitch system

1) $\lnot (A \lor \lnot A)$ --- assumed [a] 2) $A$ --- assumed [b] 3) $A \lor \lnot A$ --- from 1) by $\lor$-intro 4) $\lnot A$ --- from the contradiction : 2) and 3) by $\lnot$-intro, discharging [...
Mauro ALLEGRANZA's user avatar
9 votes

Converting Fitch to Hilbert proof

The details will vary significantly depending on your target Hilbert-style system. For convenience I shall assume one that has the usual boolean connectives instead of just a measly "$\to$". In all ...
user21820's user avatar
  • 59.1k
9 votes
Accepted

Trouble understanding proof to $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$?

The reductio ad absurdum rule RAA (I use $\ulcorner \!\cdot\! \urcorner$ to mark discharged assumptions, with a superscript to point at the discharging rule) \begin{equation} \dfrac{\ulcorner \lnot \...
Taroccoesbrocco's user avatar
9 votes
Accepted

Can anyone clarify the rules for $\forall$ intro and elimination, and $\exists$ intro and elimination?

Unfortunately, different formal proof systems will do things differently .... but here is how the book I am using ('Language, Proof, and Logic') defines these rules: First, the system makes the ...
Bram28's user avatar
  • 101k
9 votes
Accepted

The interpretation of $\nvdash$

You're exactly right - $A \not \vdash \perp$ means that $A$ is consistent. That is, we cannot derive a contradiction using $A$ as hypotheses. But there is a difference between "we can't prove it ...
Chris Grossack's user avatar
9 votes
Accepted

How do I know what assumptions I can make in a proof?

Overall, this is a $ \rightarrow $ statement; that's the last operation outside of parentheses. So for a direct proof, the last step would be $ \rightarrow $ introduction. To do $ \rightarrow $ ...
Toby Bartels's user avatar
  • 4,865
8 votes
Accepted

Why is the left-intro rule in Sequent Calculus equivalent to elimination rule in Natural Deduction?

You can say that the hypothesis $\Gamma, A \land B$ is stronger than $\Gamma, A$ because in $\Gamma, A \land B$ you have more hypotheses than in $\Gamma, A$. But the statement $\Gamma, A \land B \...
Taroccoesbrocco's user avatar
8 votes
Accepted

What if we don't accept ex falso quodlibet?

See Paraconsistent Logic for a family of logics that reject Ex Falso (aka: Principle of Explosion). See also: Walter Carnielli & Marcelo Esteban Coniglio, Paraconsistent Logic: Consistency, ...
Mauro ALLEGRANZA's user avatar
8 votes
Accepted

Proof of double negation elimination using natural deduction

The rules you list comprise a natural deduction system for intuitionistic logic. The sequent $\lnot A\to \bot\vdash A$ is not valid in intuitionistic logic, so it is not provable in your system. To ...
Alex Kruckman's user avatar
7 votes

natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

Example Let $\Gamma$ the set of first-order Peano axioms: no variables free. 1) $\Gamma \vdash \exists x (x = 0)$ --- easily provable 2) $\Gamma, x=0 \vdash x=0$ --- obvious 3) $\Gamma \vdash x=0$ ...
Mauro ALLEGRANZA's user avatar
7 votes

Calculus of Natural Deduction That Works for Empty Structures

The easiest (and in my opinion cleanest) way to do this is to augment the context. In the sequent calculus you presented, you have the left-hand of the sequent being a set $Γ$ of formulae. Instead of ...
user21820's user avatar
  • 59.1k
7 votes
Accepted

How to prove the validity of $¬∃x P(x) ⊢ ∀x ¬P(x)$ in predicate logic

We need contradiction in the proof (but it is not a poof by contradiction) : 1) $\lnot \exists x \ Px$ --- premise 2) $\quad\quad| \quad Px$ --- assumed [a] 3) $\quad\quad| \quad \exists x \ Px$ ---...
Mauro ALLEGRANZA's user avatar
7 votes

Is this proof correct? (natural deduction)

You were right to doubt your proof; it's not quite right. The main mistake is that you are effectively closing two subproofs at once once you go from 2.2.3 to 3, but you can only close one subproof ...
Bram28's user avatar
  • 101k
7 votes

Why not ban nested quantifiers over the same variable?

In your first example $y$ does not occur free in step 2 and in your second example $x$ does not occur free in step 1, so the problem is not with the variable occurrences in the antecedents to the ...
Rob Arthan's user avatar
  • 49.2k
7 votes
Accepted

What is the utility, exactly, of the Deduction Theorem?

The theorem says that to prove an implication it is enough to assume the hypothesis and proceed to prove the conclusion. Proofs of that kind tend to be more natural than proofs that conclude the ...
Andrés E. Caicedo's user avatar
7 votes
Accepted

Relationship between sequent calculus and Hilbert systems, natural deduction, etc

To define a logic you need to specify a language of formulas, and then you need to provide either 1) a semantics, or 2) a proof system (i.e. a collection of rules of inference). For commonly ...
Derek Elkins left SE's user avatar
7 votes
Accepted

If the move is correct, which rule allows to go from line 4 to line 5 of this derivation? ( a question on the use of " falsum" in natural deduction)

It is the principle of explosion, also known as ex falso quodlibert: from contradiction, anything follows. In natural deduction, it says that if $\mathcal{D}$ is a derivation with conclusion $\bot$ ...
Taroccoesbrocco's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible