Questions tagged [formal-proofs]

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

89 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
4
votes
3answers
490 views

Natural deduction proof of $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y)) \vdash \forall z.Q(z)$

My attempt $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y))$ [premise] $\forall y.P(y) \implies Q(y)$ [$\land$ elim 1] $\forall x.P(x)$ [$\land$ elim 1] $a, P(a)$ [$\forall$ elim 3] $a, P(a) \...
4
votes
0answers
371 views

Axioms of Newtonian Mechanics

Axiomatically speaking, could Newton's laws be derived (as theorems) from the conservation of momentum and energy -- along with a few suitable definitions of things like an inertia frame and force? ...
3
votes
0answers
91 views

Formal proof of $\exists x (\exists y P(y) \rightarrow P(x))$ and $(\forall x \exists y R(x,y))\rightarrow (\forall y \exists x R(y,x))$

within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \...
3
votes
1answer
210 views

Conditional Statements/ Implication statements within a proof specifically linear algebra

I am sort of new to the mathstackexchange so excuse me for any mistakes that I make while writing this post. I've been working on proofs and ran into a conflicted view of how to prove conditional ...
3
votes
0answers
130 views

Is there an intuitive way to understand the split between additive and multiplicative connectives?

For example, where $\otimes$ is multiplicative conjunction, our rules are: $$ \frac { \Gamma ,\: A,\: B\: \Rightarrow \Delta }{ \Gamma ,\: A\otimes B\Rightarrow \Delta } \quad \quad \frac { \Gamma \:...
3
votes
0answers
594 views

A simple proof of Descartes's rule of sign

I search all over the Internet for a proof of Descartes's rule of sign. Found a pdf file which has page-long proof that a high schooler has to no way to understand. Can somebody talented here give ...
2
votes
1answer
78 views

Show that the proof rule is not sound and proof question

I'm asked to show that the proof rule \begin{equation} \dfrac{\varphi \to \psi}{\lnot \varphi \to \lnot \psi} \end{equation} is not sound. To show this would I just make the truth tables for the ...
2
votes
0answers
92 views

Reference request: the space of formalisms for proving function totality

I'd like to develop an intuition about the space of axiomatic systems (formalisms) that can be used to prove totality of Turing machines. To this end, I'm interested in the set of "totality proof ...
2
votes
1answer
158 views

Fitch-style Deductive Proof

I am having trouble with the following question: Give natural deduction proofs of the following formulas (from no assumptions): $p \to p$. Here is what I have so far: $$\begin{array}{|l}\hline~~\...
2
votes
0answers
46 views

Strength of Asymmetric Tautology/Reverse Unit Propagation in proofs

Given a set of disjunctions in propositional logic, they can be said to entail another disjunction D if the negation of D, when added as a set of unit clauses to the original set, yields an ...
2
votes
0answers
67 views

Elementary Hoare logic proof

I would like to prove that the following Hoare triple is correct by giving a full Hoare logic proof. (Assuming all variables are real.) How can I do so? $$\{c = 0\} ~ a := −c; ~ b := a + c; ~ c := a ~...
2
votes
0answers
133 views

Are there any recent advances in formalizing the undecidability of $\mathit{CH}$?

I'm cross-posting this from Mathoverflow. Since I'm asking for recent developments, it seems best to have answers in both sites. The website Formalizing 100 Theorems by Freek Wiedijk contains a list ...
2
votes
1answer
409 views

Gambler's ruin: verifying Markov property

Gambler's ruin: the gambler starts with $\$i$, where $ 1<i<N$. He wins $\$1$ with probability $p$ and loses $\$1$ with probability $1-p$. When he reaches $0$ (ruin) or $N$ (win), he stops ...
2
votes
1answer
136 views

Is “forall elimination twice with the same fresh variable” allowed?

I am looking to prove that $\forall x \forall y \; P(x,y) \vdash \forall x \; P(x,x)$ and I wonder if this is allowed:...
2
votes
0answers
216 views

Hilbert style proof for $\Box A \vee \Box B \rightarrow \Box(A\vee B)$ in K.

I have to find a formal Hilbert style proof for $\Box A \vee \Box B \rightarrow \Box(A\vee B)$ on modal logic, K. I can use all classical propositional tautologies, Modus Ponens and Distribution axiom....
1
vote
0answers
37 views

What is the proof for the factorization criterion?

** The Factorization Criterion ** Let $U$ be a statistic based on the random sample $Y_1, Y_2,...Y_n$. Then $U$ is a sufficient statistics for the estimation of a parameter $\theta$ if and only if ...
1
vote
1answer
73 views

Can axioms be premises in formal proofs?

If I use an axiom to prove a theorem, i.e. use the axioms of equality in FOL to prove the converse of the axiom of extensionality, do I list those axioms as premises in a formal proof? The answer ...
1
vote
1answer
58 views

Proof of Natural Numbers using n+1 = n ∪ {n}

In set theory natural numbers are defined by 0 = ∅ and natural number n+1 = n ∪ {n} I need to prove that for every n ∈ N , n = {k ∈ N | k < n}. I know that natural numbers 1 = {∅} 2 = {∅,{∅}} ...
1
vote
0answers
70 views

Predicate Logic Hilbert Proof

In the Hilbert proof system for predicate logic, prove that the formula: $\exists x~\big(B(x)\to C(x)\big)\to\big(\forall x~B(x)\to\exists x~C(x)\big)$ I'm awful with Hilbert Proofs and have no idea ...
1
vote
0answers
30 views

Definition of the spectrum in first order logic

I want to understand the definition of the spectrum and therefore I want to know, what it means that a model has n elements or that a model is of size n. What is said to be an element? Are these only ...
1
vote
1answer
123 views

Book Recommendation

To start out with, I'm a junior in high school who is intrigued by the rigor of higher mathematics and is currently attempting to self study Volume 1 of Apostol's Calculus. I haven't had any previous ...
1
vote
0answers
57 views

Prove $\Sigma \vdash \lnot(\phi \rightarrow \psi)$ iff $\Sigma \vdash \phi$ and $\Sigma \vdash \lnot \psi.$

$\Sigma$ is a set of sentences, the set $ L$ consists of all axioms of the forms: A1) $ \ \phi \rightarrow (\psi \rightarrow \phi)$ A2) $\ (\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow (...
1
vote
0answers
32 views

How to make my analysis more rigorous?

I was dealing with 3-DOF attitude dynamics of rigid body in a geometrical framework and wanted to comment upon the following defined function $F$ at its maxima. Consider $F \in \mathbb{R} : F(e_{\...
1
vote
0answers
59 views

Deduction of $\vdash \exists x (Px \rightarrow \forall y Py)$

I was reading this question and I was curious, since I haven't quite grasp this topic being fairly new and all, how much would it differ the "tree" or list of deductions if instead of $\vdash \exists ...
1
vote
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 ...
1
vote
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 ...
1
vote
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 ...
1
vote
0answers
77 views

Formally proving that $a_i\delta_{ij} = a_j$

Using the summation convention and the Kronecker delta ($\delta$), one can show that $$a_i\delta_{ij} = a_j.$$ If one expands the expression, one is looking at $$ a_i\delta_{ij} = a_1\delta_{1j} + ...
1
vote
0answers
129 views

Stuck on proving ($p \Rightarrow q) \land (q \equiv r) \Rightarrow (p\Rightarrow r)$

I'm in a Foundations of Computer Science course and it's all about logic and proofs. Some proofs are harder than others, and I'm completely stuck on this proof. It comes out of the textbook Texts and ...
1
vote
1answer
71 views

Show that a given formula is not provable without the associative rule

This question is from Shoenfield's "Mathematical Logic", an exercise on page 25. Show that the formula $((x \neq x) \vee \neg(x \neq x \vee x \neq x)) \vee (x \neq x \vee x \neq x)$ is a theorem, ...
1
vote
0answers
38 views

How Does the Number of Lines of a Proof Change If Expanding a Condensed Detachment Proof into a Simultaneous Substitution and Detachment Proof?

For every condensed detachment proof, there exists a substitution and detachment proof. If both the antecedent of the major premise, e. g. one having form C$\alpha$$\beta$ or (p $\rightarrow$ q) ...
1
vote
1answer
63 views

Can we write formal (mechanical) proof of any theorem?

why formal proofs are not widely used? sometimes non formal proofs are cumbersome. are there any "important" theorems that have been proved formally
1
vote
0answers
267 views

If a set has an upper bound, it has infinitely many upper bounds.

Let $A$ be a subset of the real numbers, with $A \neq \emptyset$. Prove that if $x$ is an upper bound of $A$, then $A$ has infinitely many upper bounds. This seems like something that is pretty ...
1
vote
2answers
249 views

Formal deduction proof of predicates

I am trying to proof equality is transitive, that is, $\emptyset \vdash \forall x \forall y \forall z ((x=y) \land (y=z) \to(x=z))$ using formal deduction (17 rules) and also other rules (ex. To ...
1
vote
0answers
108 views

No Proof, Just Luck

I just read about the Goldbach Conjecture and it got me thinking about probabilities. Supposing that prime numbers are somewhat randomly distributed) then if we calculate the odds of a given even ...
1
vote
0answers
79 views

Isabelle and “Method of Coefficients”

I have been trying to use the Method of Coefficients in some combinatorial arguments. Since the result ended up being more complicated than I am comfortable with I would like to know if there is ...
1
vote
0answers
553 views

Existential and Universal Equivalence Proof

Taking ¬∀x:X.r≡∃x:X.¬r Is there a way of actually formally proving this? Not implementing it but proving how to go from a negated universal quantifier to a an existential with a negated element... ...
1
vote
0answers
149 views

(Another) Proof within Hilbert system

I know there are plenty of similar posts around, but I could not find an answer to this particular question (and I've been at it for two days now, getting nowhere). The proof I'm trying to construe in ...
1
vote
0answers
38 views

Logical systems and formal proof

Is there any good book dealing with various formal systems and a book for formal proofs. Or atleast some good notes. This page on wikipedia also says: 'This article needs attention from an expert in ...
1
vote
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?
1
vote
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. \ (\...
1
vote
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 ...
0
votes
0answers
45 views

how to give a formal prove to $ \vdash \exists x (P(x) \rightarrow P(y)) $

I am struggeling with giving prove for the next statement : $\vdash\exists x (P(x) \rightarrow P(y))$. This is what I have done but it fails because $\alpha$ isn't a logical sentence. $\exists x (...
0
votes
0answers
21 views

Formal Methods and specification of program

I have command $choose$ that assign one value from array ${x1...xn}$ to variable $x$. Every call it assigns the same value to the variable. I need to create the specification for this program. I ...
0
votes
0answers
72 views

Why is the calculus of constructions called that way, and what is a “construction” in CoC?

I'm reading about the calculus of construction Nederpelt & Geuvers' book "Type theory and formal proof". I can see that CoC allows us to extend the curry howard isomorphism from simply typed ...
0
votes
0answers
35 views

How do I prove relation involving inequalities is transitive?

I have only written proofs that prove relations using equality are transitive. I have no idea how to manipulate equations with inequalities. R = {(x, y) | x − y > 1} is a relation on ℝ Claim: R is ...
0
votes
0answers
29 views

How can I prove that $n \sqrt{\frac{x}{n^2}} = \sqrt{x} | n \in \mathbb{N}$?

I came across this observation in an exam today, and thought that this might be useful in making certain algorithms run faster, but first I want a way to prove that this is true. How can I do this? ...
0
votes
0answers
32 views

How do I prove using an $\epsilon - \delta$ proof that $\lim_{x\rightarrow \frac{1}{e}}(e^{x^{x^x}})<2$?

Not a homework question. Just wanting to refresh my epsilon delta proofs, and came up with this - struggled for an hour, no idea where to start.
0
votes
1answer
39 views

prove commuting quadratic functions of real numbers are equal

Suppose that $$f(x) = ax^2 +b$$ is a quadratic function, where $ (a, b) \in \mathbb R^2$ and $a \neq 0. $ If $$g(x) = cx^2 +d,$$ where $(c, d) \in \mathbb R^2$ and $c \neq 0,$ is another quadratic ...
0
votes
0answers
32 views

Reasons for formalizing mathematics

What is the motivation behind formalizing a piece of mathematics in a system like Mizar? I ask as someone interested in the process. I mean it's not like anyone is going to read those formal proofs. ...