0
votes
1answer
12 views

Struggling with proof, by contrapositive?

I am having trouble solving this proof. I tried to do a proof by contrapositive. Q = $(u+z)/(v+w) < z/w$ P = $(u/v < x/y \land x/y < z/w)$ Assuming $\lnot Q$ got me: $u/v \ge z/w$ ...
0
votes
2answers
24 views

How to quantify this statement

How do I quantify this statement? Let $x \in \mathbb{R}$. $1 \le x \le 2$ if and only if $1 \le x \le 1+ 1/n$ for some $n \in \mathbb{N}$. When I am trying to prove this, I am led (in the course of ...
2
votes
1answer
51 views

Proof negation in Gentzen system

I am provided with the L¬ and R¬ Gentzen rules for negation (besides “Cut” rule and some rules for ⋀ and →): $${\Gamma\vdash\Delta,\varphi\over \Gamma,\lnot\varphi\vdash \Delta}\ L\lnot \\[4ex] ...
1
vote
1answer
34 views

On provability within minimal logic

In its most naive form my question boils down to this: when is a proposition that is provable "by contradiction" also provable "directly"? IOW, is it possible to know, a priori, that a ...
0
votes
3answers
133 views

Using rules of inference (Leibniz) to prove theorems.

Leibniz: If $A \equiv B$ is a theorem, then so is $C[p:= A] \equiv C[p:= B]$. Note: p is "fresh" means p doesn't occur in $A, B, C$. I am trying to understand how to use Leibniz rule of inference for ...
0
votes
1answer
47 views

Prove by Hilbert deduction: ⊢∃x(AvB)→(∃xAv∃xB); ⊢(∃xAv∃xB)→∃x(AvB)

I'd really like your help proving: 1)⊢∃x(AvB)→(∃xAv∃xB) 2)⊢(∃xAv∃xB)→∃x(AvB) Our proof system contains next Hilbert's axioms: 1.A→(B→A) 2.(A→B)→((A→(B→X))→(A→X)) 3.(A&B)→A 4.(A&B)→B ...
3
votes
1answer
102 views

Type Theory (Proof tree)

Suppose $B(x)$ set $(x:A)$ is a family of sets and $D$ is a set. Prove $(\Sigma x:A)B(x) \times D \to (\Sigma x:A)(B(x) \times D)$. Using the so called Curry-Howard correspondence one may ...
9
votes
3answers
289 views

Prove by Hilbert deduction: $\vdash _{HFOL} \forall x (\neg(A \to \bar{B}))\to \neg(\forall xA \to \neg(\forall xB))$

I'd really like your help proving: $\vdash_{HFOL} \forall x (\neg(A \to \bar{B}))\to \neg(\forall xA \to \neg(\forall xB))$ Where $HFOL$ is the proof system which contains the Hilbert relevant ...
43
votes
13answers
2k views

What is a proof?

I am just a high school student, and I haven't seen much in mathematics (calculus and abstract algebra). Mathematics is a system of axioms which you choose yourself for a set of undefined entities, ...
2
votes
1answer
88 views

What is the difference between $Γ⊭Φ$ and $Γ⊭¬Φ$?

Did I understand this correctly? $Γ⊨Φ$ ($Φ$ is considered true) $Γ⊨¬Φ$ ($Φ$ is considered false) $Γ⊭Φ$ ($Φ$ is considered neither true nor false) $Γ⊭¬Φ$ ??? Please help me understand. How can ...
1
vote
0answers
66 views

Examining every mathematical result in purely formal, ZFC language.

My main interest is physics. However, being self-taught in mathematics for the most part, my proofs tend to be more intuitive than it is acceptable. Yet, I recognize my inaptitude in rigor, and I ...
134
votes
13answers
5k views

Can every proof by contradiction also be shown without contradiction?

Are there some proofs that can only be shown by contradiction or can everything that can be shown by contradiction also be shown without contradiction? What are the advantage/disadvantages of proving ...
1
vote
1answer
319 views

proof of validity of tautology in first order logic

Every first-order logic formula which has a tautological shape in propositional logic is a valid formula. Will it be possible to give a formal proof for the above ? Thanks and Regards.
0
votes
2answers
165 views

is it possible to prove the method of mathematical induction itself?

Since the method of mathematical induction follows some sort of 'algorithm', would the method itself be provable? namely, give that the method of mathematical induction is as follows: if S is a ...
9
votes
2answers
1k views

How can I learn about proofs for computer science?

I study computer science at a university. My school offers several courses where various proofs are expected, but there is no course that introduces the fundamental concepts of proofs and how to write ...