Proof theory is an area of logic that studies proof as formal mathematical objects. If you'd like advice on the presentation of a proof you have in draft, use proof-writing instead. If you'd like feedback on its validity, use proof-verification. If none of the above apply, you do not need a proof-* ...

learn more… | top users | synonyms

0
votes
0answers
45 views

Euler - Lagrange Equations proof

I have been searching on the internet about Euler - Lagrange Equations and I didn't find anywhere the proof for Euler - Lagrange Equations. I need to find a proof for this equations. From where can I ...
2
votes
1answer
59 views

Examples of theories with enough constants

A theory $\Gamma$ of $L$-sentences has enough constants if for every $L$-formula $\phi(x)$ with one free variable $x$, there is a constant $c$ such that $$\Gamma \vdash \exists x \phi(x) \rightarrow ...
2
votes
2answers
93 views

How does the Soundness Theorem follow from this lemma?

The soundness theorem is a famous theorem in logic that goes like this: If $\Gamma \vdash \phi$, then $\Gamma \vDash \phi$. It's supposed to follow readily from Lemma 3.2.3 from Moerdijk/Van ...
2
votes
2answers
137 views

Proof of completeness and soundness of a proof system

As stated here, https://en.wikipedia.org/wiki/List_of_rules_of_inference, "a set of rules can be used to infer any valid conclusion if it is complete, while never inferring an invalid conclusion, if ...
0
votes
2answers
72 views

Decidability of certain first-order statements

Is it possible to construct an algorithm that can formally prove any statement in some countable first-order theory except for exactly those which aren't provable in the theory? Why or why not? Edit: ...
2
votes
3answers
62 views

Prove that $f(x,y,z)$ is reducible if and only if $a,b,c,d$ is a geometric progression.

Let $a,b,c,d$ be real numbers not all $0$, and let $f(x,y,z)$ be the polynomial in three variables defined by $$f(x,y,z) = axyz + b(xy + yz + zx) + c(x + y + z) + d.$$ Prove that $f(x,y,z)$ ...
2
votes
0answers
29 views

Disequality in Type Theory [duplicate]

Is it possible to prove $0 \neq 1$ in (non-univalent) Martin-Löf type theory, where $0$ and $1$ are natural numbers (defined using the usual inductive type $0 : \mathbb{N}$, $S : \mathbb{N} \to ...
1
vote
2answers
64 views

Inconsistent theory with uniformly long refutation?

I understand that there are theorems in PA that necessarily require "very long" proofs; cmp. [1]. On the other hand it seems interesting to think about Life in an inconsistent world. So is it ...
5
votes
3answers
215 views

Why can't you prove the law of the excluded middle in intuitionistic logic (for layman)?

I am learning about the difference between booleans and classical logics in Coq, and why logical propositions are sort of a superset of booleans: Why are logical connectives and booleans separate in ...
0
votes
1answer
22 views

Can we extend NP-HARD proof of one problem to another?

I have tried to put my question in following diagram I have two domains A and B. I can formulate two optimizations problems 1 and 2. In domain A, efficient algorithms exist for solving these two ...
2
votes
1answer
65 views

Why does the dependent product type need “forall”?

I feel stupid asking this question because it is so fundamental to logic and math. However, in my starting to learn proof theory and now type theory, I have not seen an explanation on why you need the ...
5
votes
1answer
99 views

Completeness for Infinitary Logic?

I have heard a rumor that there is a proof system for certain infinitary logics, given by Carol Karp (?) in her thesis, but I can't find a copy. The result that I'm told exists is the following: A ...
5
votes
2answers
109 views

Is it possible to nonconstructively prove that a statement can be proven or disproven within a formal system?

I've heard of many examples of statements that have been proven to be independent of a formal system, meaning that they can't be proven within that formal system (for example, the Continuum Hypothesis ...
1
vote
1answer
82 views

Natural deduction proof from falsehood

How does a natural proof of $⊥\rightarrow A$ (let $A$ be an arbitrary formula) look like in the classical calculus of natural deduction? Thanks
0
votes
0answers
42 views

Pythagorian theorem in language of Hilbert's system of geometry

How can one formulate the Pythagorian theorem in the language of Hilbert's system of geometry? How can one speak about the length of the hypotenuse for example?
7
votes
1answer
130 views

WLOG and “by symmetry” arguments and the foundations of mathematics

John Harrison's paper Without Loss of Generality raises the interesting point that although "without loss of generality"/"by symmetry" arguments are a common proof technique, there is no corresponding ...
-1
votes
2answers
142 views

Can all theorems be deduced directly from the ZFC axioms?

I stumbled upon a website called metamath that claims to be able to do this : http://us.metamath.org/mpegif/mmset.html
0
votes
0answers
49 views

Proof of cut elimination

I am reading Proofs and types and am blocked at the proof of cut elimination in sequent calculus (chap 13). I don't see either how the cuts are being pushed up above the preceding steps to the top of ...
7
votes
4answers
335 views

mathematical proof vs. first-order logic deductions

For a long time I thought that the standard mathematical proofs, only were an informal or imperfect way of writing the proof in the language of first-order logic. When I say standard mathematical ...
2
votes
0answers
49 views

Proof by reflection and Homotopy Type Theory

I have been looking into various proof assistants, and came across the method of proof by reflection in Coq, which (from what I understand) allows one to verify a program provides the correct "answer" ...
0
votes
1answer
43 views

How to show that the displaying numbers of a onto function is k!S(n,k)?

Let it be $A$,$B$ sets that $|A|$=$n$, $|B|$=$k$ and $|A|>|B|$. How to show that the displaying numbers of an onto function $f$:$A$ $\rightarrow$ $B$ is: $\begin{Bmatrix} n \\ k\end{Bmatrix}$$k!$ ...
2
votes
1answer
67 views

prove that this number contains two equal digits

We delete the first digit from the number $7^{1996}$ and then we add it to the remaining number, repeat this until we get a number consisting of $10$ digits, prove that, this number contains two equal ...
-1
votes
2answers
63 views

Prove that to any three numbers positive integers [closed]

Prove that for any three positive integers, following equality holds $$\operatorname{lcm}(ab , bc , ca ) \cdot \gcd(a , b, c )=abc$$
2
votes
1answer
76 views

Proving a trigonometric identity with tangents [closed]

Prove that: $$\tan^227^\circ +2 \tan27^\circ \tan36^\circ=1$$ any help, I appreciate it.
2
votes
5answers
208 views

Rigorous proof of '${\{A \Rightarrow B}\} \iff {\{\neg B \Rightarrow \neg A}\}$' for a high school student

One method to prove the statement 'If A, then B' is to prove that 'If not B, then not A'. First time that I saw this method it was not (and still isn't) obvious. So I used a more obvious example to ...
2
votes
4answers
268 views

How do I know which of these are mathematical statements?

While reading this book called "How to Read and do Proofs" by Daniel Solow(Google) I found the following exercise at the end of the first chapter. So how do I know if something is a mathematical ...
1
vote
2answers
176 views

Is Fermat's Last theorem equivalent to $1 + 1 = 2$? [closed]

I got into a debate with someone concerning whether FLT is equivalent to $1 + 1 =2$. He said common sense tells us it isn't equivalent. However, I disagreed. Since both are provable statements, they ...
2
votes
1answer
91 views

Can we see natural deduction rules as functions or even as formal grammars?

Is there a way of seeing natural deduction rules as functions or even as formal grammars, maybe context-free grammars or Lambek grammars? It seems quite "easy" to see the rules as functions which take ...
0
votes
1answer
71 views

Using Sequent Calculus to prove $\exists x_1 x_2 [ B ( x_1 , x_2 ) \rightarrow \forall y_1 y_2 B ( y_1 , y_2 ) ]$

I need to prove the validity of the following formula using the sequent calculus LK: $$ \exists x_1 x_2 [ B ( x_1 , x_2 ) \rightarrow \forall y_1 y_2 B ( y_1 , y_2 ) ] \text{.} $$ I already had a look ...
2
votes
2answers
70 views

Explanation on the symmetry between identity axiom and cut rule

In Proofs And Types at the beginning of 5.1.4 Girard says that the identity axiom is somewhat complementary to the cut rule, more specifically 'The identity axiom says that $C$ (on the left) is ...
5
votes
2answers
352 views

What does “rigorous proof” mean?

I have heard several times that some mathematician has given another and more rigorous for an established theorem, but I don't know what does it really mean and what differences makes it to be more ...
0
votes
1answer
32 views

Problem with a step in a proof in predictive control

I'm trying to follow a demontration written in an optimal control paper. In one of the steps, it states What I'm having troubles with is the last step, it states that because of the convexity of ...
5
votes
0answers
72 views

What are some arguments/counterarguments for Zeilberger's “proof certificates”?

Here is the quote I wish to ask about: "I speculate that similar developments will occur elsewhere in mathematics, and will 'trivialize' large parts of mathematics, by reducing mathematical ...
2
votes
1answer
69 views

Encyclopedia of Mathematical Proofs with no English

I was wondering if anyone is aware of a modern book that builds a subset of elementary number theory from Peano axioms preferably in a Principia Mathematica fashion? Or similarly an encyclopedia of ...
0
votes
0answers
30 views

Is it always possible to algebraically express a function defined by a set of rules?

Let's say you have an arbitrary function defined by a set of rules such that for example: Domain $\hspace{9mm}$ Range $\hspace{5mm}$ 1 $\hspace{23mm}$ 2 $\hspace{5mm}$ 2 $\hspace{23mm}$ 2 ...
3
votes
1answer
97 views

Consistent, complete axiom system that proves its own consistency

Is there a consistent, complete axiom system that proves its own consistency? I know that this question isn't exact and I haven't defined when an axiom system proves its own consistency because ...
0
votes
1answer
65 views

What kind of trivial statement still needs to be proven?

There are many statements that seem to be needless of a proof since they are ‘evident’ mainly because of our intuition. But some of them have proofs. For example, in C. Adams’ Introduction to ...
2
votes
0answers
44 views

Clever proofs that prove one identity is equal to another, without going through the original identity?

In a previous question I attempted to formalize the argument of going from one proof of an identity to another, which turned out to be harder than I thought. The thing is, while it may be impossible ...
2
votes
0answers
35 views

Is it always possible to go from one identity to another?

This question was inspired by this Quora question. I'm sure lots of you are familiar with the fact that we have many different representations of $\pi$, things like $$ \begin{align} \pi & = ...
1
vote
7answers
287 views

Prove $ \{(p \lor q) \land (p \implies r) \land (q \implies r) \} \implies r$ is a tautology using logical properties

I spent quite a bit of time on this and have little to no ideas on how to proceed. Using the conditional laws and De Morgan's law, I got to $$( \sim p \land \sim q) \lor (p \land \sim r) \lor(q ...
1
vote
1answer
39 views

Isomorphic: Properties Proved for A are True for B?

To make this a little more concrete, consider vector spaces. An isomorphism between two spaces is an invertible linear transformation. It seems to then be commonly asserted or assumed that if A and ...
1
vote
1answer
67 views

Using the notion of provability only, how to show that $\Gamma \nvdash \varphi$?

For a practical example, suppose I want to show that $\{ P\} \nvdash Q$. From completeness, this is trivial: just find a model where $P$ is true and $Q$ false. But suppose I am stubborn and I don't ...
3
votes
2answers
80 views

Proving that $\sum_{i=2}^n(5i-4)=\frac{n(5n-3)-2}{2}$ for all $n\geq 1$ by mathematical induction

I have this question: Show, using mathematical induction, that for all natural numbers $n$, $$6 + 11 + 16 + 21 + \cdots + (5n-4) = \frac{n(5n-3)-2}{2}$$ I am confused in that that question states ...
3
votes
3answers
92 views

If $T$ a consistent set of sentences and $a,b$ sentences such that $T\vdash (a\rightarrow b)$and $T\vdash (\lnot a\rightarrow b)$ Then $T\vdash b$ [closed]

I am stucked at this problem for a long time: Let $T$ be a consistent set of first-order sentences and let $\alpha,\beta$ be sentences. Prove that if $T\vdash( \alpha\rightarrow \beta)$ and ...
2
votes
2answers
96 views

Prove by Natural deduction that $\lnot\exists xP(x)\rightarrow\forall x\lnot P(x)$

I got this problem: Prove by Natural deduction in First Order Logic that $\lnot\exists xP(x)\rightarrow\forall x \lnot P(x)$ I tried to prove it using the Contradiction Theorem but I got ...
3
votes
1answer
70 views

What exactly is wrong with this argument (Lucas-Penrose fallacy)

Argument "For every computer system, there is a sentence which is undecidable for the computer, but the human sees that it is true, therefore proving the sentence via some non-algorithmic method." ...
0
votes
1answer
119 views

Mathematical Induction. Horses made me question my understanding [duplicate]

I recently read about the false inductive proof that all horses are the same colour. There are some mathSE threads about this already (MathSE_thread_1, MathSE_thread_2). After reading this, I now ...
10
votes
0answers
213 views

The ethics of Borel determinacy

I was speaking with a friend the other day, and I happened to say "morally, Borel determinacy is as strong as ZF." I was riffing on the well-known result of Harvey Friedman, that we need ...
2
votes
1answer
84 views

Left and Right hand associativity equivalent first order logic

Say we are in a first order theory, and one of our inference rules is the associative rule saying that we can infer $(A \vee B) \vee C$ from $A \vee (B \vee C)$. Using the other logical inference ...
1
vote
0answers
19 views

Showing that language $L^{'}$ is regular given $L$ is regular [duplicate]

Say $L \subseteq \{a,b\}^*$ is a regular language with words whose length is divisible by 3. Each word $w \in L$ has the form $w=xyz$ with $|x|=|y|=|z|$, where $y$ is then called the middle third of ...