# 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
3answers
490 views

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 ...
0answers
130 views

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 ...
0answers
67 views

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 ...
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, ...
0answers
38 views

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 ...
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 ...
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 ...
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? ...
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.
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 ...
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. ...