Questions tagged [natural-deduction]

For questions concerning natural deduction, a formal proof system studied in proof theory. A natural deduction proof starts with a set of premises and applies introduction and elimination rules to arrive at the conclusion. This tag is not specific to any particular logic, classical or intuitionistic, propositional or allowing quantifiers.

Filter by
Sorted by
Tagged with
0 votes
2 answers
102 views

Help proving $\lnot$(G $\rightarrow$ $\lnot$A) $\vdash$ G.

I'm have been working on a natural deduction assignment for a couple of days and I went yesterday to ask my teacher for help but he gave me no helpful information so I'm asking here. I have tried a ...
user59854's user avatar
5 votes
0 answers
163 views

Proving $\exists x[P(x)] \to \exists y[\exists x[P(x)]\to P(y)]$ in for intuitionistic $\varepsilon$-calculus.

I am researching Mint's paper: Intuitionistic Existential Instantiation and Epsilon Symbol (this is as far as I know unfinished work) In intuitionistic logic, it is not difficult to prove that $$\...
Tungsten's user avatar
  • 130
2 votes
2 answers
56 views

Proving conjunction introduction in a natural deduction system with negation and disjunction

I'm stuck solving the following problem from Goldrei's Propositional and Predicate Calculus (p. 131): $L$ is a propositional language based on the connectives $\lnot$, $\lor$. A system $S$ for $L$ ...
user245312's user avatar
1 vote
1 answer
148 views

Provided with the $\leftrightarrow$ elimination rule, is the substitution rule still neccessary in a natural deduction system?

Analogous to the substitution rule for the equality symbol in FOL, it looks natural to have a substitution rule for the $\leftrightarrow$ symbol in propostional logic, i.e., from the formula ...A... ...
William's user avatar
  • 205
0 votes
1 answer
102 views

A natural deduction proofs using only 11 inference rules and no axioms [closed]

In this Wikipedia page https://en.wikipedia.org/wiki/Propositional_calculus, specifically in the section "Example 2. Natural deduction system", it mentions 11 inference rules and no axioms ...
Ahmed 's user avatar
  • 19
4 votes
1 answer
383 views

Are there axioms in a natural deduction system?

In the Hilbert system, a proof may include some axioms. In a natural deduction system, it seems no axiom is involved, at least from the examples I read in logic books. So, I wonder how axioms such as ...
William's user avatar
  • 205
2 votes
2 answers
133 views

Natural deduction - prove a theorem

I am currently taking a course in "Introduction to Mathematical Logic" and I have been trying to do this proof, but everything I did just lead me to nowhere... Could anyone give me a ...
Ifkele555's user avatar
1 vote
1 answer
102 views

Proving ∀xFx v ∃x~Fx from no premises

Since there are no premise, the only way to prove must be by way of contradiction, which is to assume ~(∀xFx v ∃x~Fx). Naturally, one would expand this statement by de Morgan’s law: ~∀xFx v ~∃x~Fx and ...
MacLane's user avatar
  • 21
0 votes
0 answers
73 views

Natural deduction proof unsure if correct

I'm unsure if this method of natural deduction is correct. To prove: $P \vee F,\; \neg T \mathbin\rightarrow \neg P,\; T \mathbin\rightarrow B,\; \neg F \;\vDash\; B$ Proof: $P \vee F$ (Data) $\...
mo20045's user avatar
0 votes
2 answers
327 views

Natural Deduction Proof: (A ∨ B) ∧ (A ∨ C) ∴ A ∨ (B ∧ C)

I've been having trouble figuring out how to prove the above statement. Frankly I'm only certain in my work insofar as splitting up the premise statement into (A v B) and (A v C). I've tried using ...
Daniel Nikitin's user avatar
3 votes
3 answers
184 views

What is an example of a proof that uses the principle of explosion/ex falso quodlibet?

I am reading through Mathematical Logic by Ian Chiswell and Wilfrid Hodges. In chapter 2 they introduce natural deduction rules. Before stating a rule, the authors (usually) motivate the rule by ...
Artyom Elessar's user avatar
1 vote
0 answers
59 views

What is the justification for the RAA rule, and how does it relate to the Principle of Explosion? (Mathematical Logic by Chiswell and Hodges) [duplicate]

I am reading through Mathematical Logic by Ian Chiswell and Wilfrid Hodges and am trying trying to finalize my understanding of the RAA rule introduced in section 2.6. The book states the rule in the ...
Artyom Elessar's user avatar
1 vote
3 answers
119 views

How do we know that the negation of a statement is unique? (Mathematical Logic by Chiswell and Hodges)

I am reading Mathematical Logic by Ian Chiswell and Wilfrid Hodges and have been trying to solidify my understanding of pages 24-26 (Section 2.6 - Arguments using 'not'). In this section, the authors ...
Artyom Elessar's user avatar
0 votes
1 answer
76 views

How To Prove This Simple Theorem Using Fitch Natural Deduction System

Lemma. $ (p \land q) \iff (p \land q \land r) \lor (p\land q\land \lnot r)$ It is clear to me how this is true, but I don’t know how to prove it using only the rules of Fitch-style natural deduction. ...
Amjad's user avatar
  • 15
0 votes
0 answers
78 views

Validity of Deductive Arguments

I’ve been reading some mathematical logic texts and encountered differences in the definition of the validity of arguments, as presented below An argument is valid iff it is impossible for all the ...
William Wei's user avatar
2 votes
2 answers
748 views

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

I'm given this proof and am told to prove by deduction: $(p∨(q∧r))→(((q∧r)→p)→p)$ I have the following rules that I can use: ∧ introductions and eliminations ∨ introductions ∨ eliminations (a case ...
Colin Lightfoot's user avatar
0 votes
0 answers
78 views

Understanding the definition of $\neg \phi$, and (RAA), in Mathematical Logic by Chiswell and Hodges

I am working through Mathematical Logic by Chiswell and Hodges and am stuck on pages 24-26 (Section 2.6 - Arguments using 'not'). This section starts off by stating that "If $\phi$ is a statement,...
Artyom Elessar's user avatar
1 vote
2 answers
81 views

Natural deduction (Proof tree)

It's not clear for me how to represent the proof tree of a sequent that doesn't use and hypothesis, for example: $p \vdash q \rightarrow p$. The problem is that $q$ should appear as hypothesis to ...
Hackerman's user avatar
0 votes
1 answer
81 views

How to prove that a formula is intuitionistically valid using Kripke semantics?

I want to know how to use Kripke semantics so that I can prove that a formula is intuitionistically valid. I think that all others cases will clear out if I understand the case of implication. Let's ...
Νικολέτα Σεβαστού's user avatar
2 votes
1 answer
72 views

Intuitionistic proof of $((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$

I need to prove that the $\psi=((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$ is intuitionistically valid. I tried using the topology of open sets of $\mathbb{R}$ and an arbitrary valuation, ...
Νικολέτα Σεβαστού's user avatar
0 votes
0 answers
61 views

Natural deduction proof of $ \neg q \Rightarrow p$ using $ (p \Rightarrow q) \Rightarrow p$

I am having some trouble completing this proof, I have attached an image of my best attempt so far but I am unsure if it is correct. I would like some help on where I have gone wrong and some ideas on ...
just_some_guy's user avatar
0 votes
0 answers
43 views

Deducing $(\forall x . P) \implies P$ in minimal logic if P does not depend on any variable.

This might be a bit of a dumb question, but after pondering for a while I can't arrive to a conclusion which satisfies me. In minimal logic, the elimination rule for $\forall$ is as follows: $\forall ...
Nicky García Fierros's user avatar
1 vote
0 answers
71 views

Deduction Theorem proof issue [duplicate]

I restudied deeply logic (from scratch) and set theory (ZFC) but I came across 2 issues: In propositional logic, we prove the Deduction theorem using induction, but induction itself is proved using ...
Predator Monarch's user avatar
0 votes
1 answer
36 views

Formal deduction of some basic identities that rearrange the universal quantifier

One such identity is ∀x(a→R(x)) ↔ (a→ ∀xR(x)) Where x doesn't occur free in a. Naturally, I tried separating the two directions. So for example, in one direction we assume {∀x(a→R(x)), a} and wish ...
Nicholas's user avatar
-3 votes
1 answer
71 views

How to derive $A$ from $A$ in First Order Logic [closed]

I want to derive $A$ from $A$, here is what I have done : A hypothese $A$ (AA) 1.1 $¬A$ (AA) 1.2 $A$ (Negation Elimination from 1.1) $A -> A$ (Introduction -> (1-1.2)) $A$ (MP(0,2)) Is this ...
Lzkb's user avatar
  • 31
1 vote
1 answer
87 views

Deductively prove that $ \vdash (p \land q) \rightarrow p$

I need to prove that this is a tautology (without using truth tables, i.e. deductively), because I need to use it for another proof. $$\vdash (p \land q) \rightarrow p$$ I'm allowed to use the ...
l0ner9's user avatar
  • 623
0 votes
0 answers
36 views

Does Substitution of Logical Equivalents hold for minimal logic?

Suppose that minimal logic proves that $\psi_1\leftrightarrow\psi_2$, does it follow that minimal logic proves $\varphi[\theta/\psi_1]\leftrightarrow\varphi[\theta/\psi_2]$?
IllogicalUser's user avatar
0 votes
0 answers
72 views

Prove $\exists$-$E$ can be derived from $\forall$-$E$ and $\forall-I$

Here are the definitions of the rules: This answer helped me to prove the $\exists$-$I$ rule, but im struggling to prove $\exists$-$E$ How to show that the introduction and elimination rules for $\...
lightyourassonfire's user avatar
1 vote
1 answer
59 views

Proof by contradiction for general formulas

I have been examining the tool of proof by contradiction. $\Gamma\vdash\lnot\varphi$ iff $\Gamma\cup\{\varphi\}$ is inconsistent. This is a very natural tool, and makes sense for closed formulas $\...
Dror Tal's user avatar
0 votes
2 answers
129 views

Natural deduction proof: $(A \lor B) \land (A \lor C) \vdash A \lor (B \land C)$

My way that didn't work: \begin{align*} 1. & \quad (A \lor B) \land (A \lor C) & \text{Premise} \\ 2. & \quad A \lor B & \text{E $\land$ 1} \\ 3. & \quad [A & \text{Hypothesis} ...
Gabriel Almeida's user avatar
1 vote
3 answers
87 views

Proving $\vdash \exists x(P(x)\lor Q(x))\Leftrightarrow \exists xP(x)\lor \exists xQ(x) $ using natural deduction, forward direction attempt.

$$ \vdash \exists x(P(x)\lor Q(x))\Leftrightarrow \exists xP(x)\lor \exists xQ(x) $$ I'm unsure about a step in my (forward direction) attempt in solving this using natural deduction proof: Forward ...
Cal's user avatar
  • 23
8 votes
6 answers
2k views

Asserting that when (P→Q) and (Q→R) are true, then so is (P→R)

I am going through Velleman's "how to prove it", and am stuck on Problem 16 in section 3.2, which requires me to show, with the help of truth tables, that if $P\rightarrow Q$ and $Q\...
eeqesri's user avatar
  • 711
0 votes
0 answers
59 views

Can the rules of inference of propositional logic be applied to open formulae in first-order logic?

Where $a$ and $b$ are free variables: $\forall xPx$ Premise $Pa$ Universal Instantiation 1 $Pb$ Universal Instantiation 1 $Pa\land Pb$ Adjunction 2,3 $\forall x(Px\land Pb)$ Universal Generalization ...
Isaac Sechslingloff's user avatar
2 votes
1 answer
70 views

Find a derivation for$\{\varphi \Rightarrow (\psi \land \phi)\} \vdash \psi \to (\varphi \Rightarrow \phi)$

I was given the following problem: Find a derivation for$\{\varphi \Rightarrow (\psi \land \phi)\} \vdash \psi \Rightarrow (\varphi \Rightarrow \phi)$ The derivation is to be made using natural ...
lafinur's user avatar
  • 3,172
0 votes
1 answer
46 views

Natural deduction problem: incomplete derivation

Consider the following derivation of natural deduction: Context: This is from a problem that asks for the student to "complete" the derivation, annotating its steps and any hypothesis ...
lafinur's user avatar
  • 3,172
4 votes
1 answer
145 views

Linear logic as Fitch-style natural deduction?

I've recently been looking into linear logic, and it seems every source I can find on it uses the sequent calculus proof system. However, I personally find the sequent calculus to have numerous ...
Nico's user avatar
  • 452
0 votes
4 answers
141 views

Use natural deduction to prove ((¬P ∧ ¬Q) → ¬(P ∨ Q)) using primitive rules only

Here is my attempt which is obviously full of errors. I saw another post that has quite a similar question but I could not understand it still..
Dabria's user avatar
  • 11
0 votes
1 answer
116 views

Help with Formal Proof using introduction and elimination rules

I need help with a proof where the premise is $\lnot A \land \lnot B$ and the goal is $\lnot (A \lor B)$. We are allowed to use the introduction and elimination of the following operators: $\lnot$,$\...
Meraz Hossain's user avatar
0 votes
2 answers
121 views

Prove that $¬(A → B) ⊢ ¬(¬A ∨ B)$ in natural deduction

I just can’t seem to find a way to prove $¬(A → B) ⊢ ¬(¬A ∨ B)$ Any help would be appreciated! I am using a reductio strategy. I have made the following assumptions: $ \text{1.} ¬A ∨ B$ $ \text{2.} ¬A$...
StudentusErasmusMontanus's user avatar
0 votes
0 answers
62 views

Proof in Natural Deduction, Sequent Calculus or Hilbert System

Is there any smart way to check if certain statements are not provable in any of these proof systems? Like for example the following task: Prove or disprove the following statements: $\vDash \exists ...
jjbinks's user avatar
  • 71
1 vote
0 answers
104 views

Soundness and completeness of Fitch-style for first order logic

I am looking for literature in which a detailled proof of the soundness and completeness of Fitch-style proofs for first order logic is given. In his 1952 book "Symbolic Logic, An Introduction&...
user11718766's user avatar
3 votes
1 answer
151 views

How/where is this technique generalised and proven for other (standard, first order) logical operations (if possible)? A method of natural deduction.

Logic is something I am entirely self-taught in. Due to my resulting ignorance, it is difficult for me to search for the right things. Therefore, please excuse me if this has been asked before. The ...
Shaun's user avatar
  • 44.4k
2 votes
0 answers
96 views

Can this rule of inference do replace axiom of extensionality?

If I replace the below axiom in ZFC (or NBG) by the below inference rule, there are any consequence in what can be demonstrated? Axiom: If two sets (or classes) have the same elements then their are ...
I.F.F. dos Santos's user avatar
0 votes
1 answer
77 views

How to prove ¬p ∧ ¬q ⊢ ¬(p ∨ q) by natural deduction?

Here's my attempt, but I think it's incorrect because I don't discharge assumption 1: ¬p ∧ ¬q $\qquad$ premise ¬p $\qquad$ by (∧E) ¬q $\qquad$ by (∧E) p $\qquad$ assumption¹ p ∨ q $\qquad$ ...
Jonas's user avatar
  • 307
0 votes
1 answer
158 views

How to prove $\neg q \rightarrow \neg p \vdash p \rightarrow q$ and $\neg (p \lor q) \vdash \neg p \land \neg q$ by natural deduction?

For the first proof, I actually finished but I'm not sure if it is correct. Proof for $\neg q \rightarrow \neg p \vdash p \rightarrow q$: $\neg q \rightarrow \neg p$, $[p]^1$, $[\neg q]^2$ $\neg p$ by ...
Jonas's user avatar
  • 307
0 votes
0 answers
76 views

What does it mean to discard a hypotesis in a natural deduction?

My textbook says that in the deductive system of natural deduction every hypotesis must be discarded by a rule of inference and after being discarded, it cannot be used again in the deduction... But ...
Jonas's user avatar
  • 307
1 vote
1 answer
130 views

Trying to understand "Deriving natural deduction rules from truth tables" and having trouble with false hypothetical judgments

For rows of the truth table where the connective is false the connective is placed as a judgement. This doesn't make sense to me. Having the false proposition be in the hypothetical position makes ...
Sandy Vanderbleek's user avatar
0 votes
1 answer
113 views

Prove that contrapositive rule is equivalent to the rule of double negation

Many deduction systems I see at various places (for example here includes the following two axioms $$ a \Rightarrow (b \Rightarrow a),\\ [a \Rightarrow (b \Rightarrow c)]\Rightarrow [(a\Rightarrow b) \...
Ma Joad's user avatar
  • 7,282
2 votes
1 answer
74 views

Proof of distributivity of $\land$ over $\lor$ using disjE in natural deduction

I'm learning about natural deduction from https://www.inf.ed.ac.uk/teaching/courses/ar//slides02.pdf I'm trying to understand its proof of $$ P \land (Q \lor R) \vDash (P \land Q) \lor (P \wedge R) $$ ...
Michal Charemza's user avatar
1 vote
1 answer
167 views

How do we know inference rules are correct?

I know axioms are statements which are assumed to be true (meaning that axioms are not proved). Theorems are statements which can be proved or has been proved. In the proofs of theorems we can use ...
user859v's user avatar

1
2 3 4 5
19