# Questions tagged [formal-proofs]

For questions about proofs within a formal system, such as natural deduction or Hilbert system.

536 questions
Filter by
Sorted by
Tagged with
1answer
78 views

0answers
32 views

2answers
47 views

### What is a gross-looking formal axiomatic proof for a relatively simple proposition?

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if ...
1answer
249 views

### Question on proving validity in predicate logic

Using the proof rules of predicate logic prove the validity of the following sequent: $$\forall X \exists Y(P(X)\lor Q(Y))\vdash \exists Y \forall X(P(X)\lor Q(Y))$$ I have been trying to prove ...
0answers
61 views

### Distinction between “implicit” and “explicit” formal proofs

Can anyone comment on the distinction between two different methods of formal proof? Since I'm pretty shaky on the methods and terminology of Proof Theory I a refer to them below as the "implicit" and ...
0answers
71 views

### Why, intuitively, are propositional resolution proofs so long?

I'm trying to gain an intuitive understanding of why propositional resolution proofs tend to be so long. As every essential prime implicant can be produced via resolution, intuitively I would have ...
0answers
77 views

1answer
719 views

Let's have an vector of natural numbers $[v_1, ..., v_N]$ my goal is to show that $$\sum_{i=1}^{N-1}|v_i - v_{i+1}| \ge v_{max} - v_{min}$$ where $v_{max} = \max_{i\in1...N}(v_i)$ and $v_{min} = \... 1answer 87 views ### Prove formally that$\frac {n^2 + 2}{3n^3 - 5n}\to 0$as$n \to \infty$. I'm reviewing some Sequences notes from a Mathematics Analysis course I'm taking. I'm finding the beginning of the formal proof below confusing. Some clarity on the following questions would be much ... 2answers 628 views ### How to prove this using natural deduction $$⊢ P ∨ ¬P$$ I found this question on the net. I know the solution, but I find it complicated. How should I approach this sort of question? Or can you provide me with another solution? 1answer 122 views ### Easy question on Logic and Modes Ponens I got confused with these: using ONLY this three axioms and Modus Ponens:$$1. \ F \implies (G\implies F) \\ 2. \ (F \implies (G\implies H))\implies ((F \implies G)\implies (F \implies H)) \\ 3. \ (\... 2answers 146 views ### What's the strength of logic without$\neg\neg\exists x P(x) \implies \exists x P(x)$? As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement$\exists x:P(x)$only by constructing an explicit such object$x$, right? ... 3answers 293 views ### Giving a formal proof of p ⇒(q ⇒ r)$\vdash\$ (p ⇒ r)∨(q ⇒ r) using the rules of inference.

I can prove this with semantic equivalences and truth tables but I'm struggling on the formal proof using rules of inference front. Given its format I would assume it must finish on V-introduction ...