# Questions tagged [formal-proofs]

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

531 questions
Filter by
Sorted by
Tagged with
175 views

### Stuck on formal proof, missing one step

I'm stuck on what to put for step 7. Thank you! Horned(c) → (Elusive(c) ∧ Dangerous(c)) (Elusive(c) ∨ Mythical(c)) → Rare(c) Mammal(c) → ¬Rare(c) Horned(c) Mammal(c) ¬Rare(c) (→ Elim 5, 3) ? ⊥ (...
209 views

### Stuck on Formal Proofs

I'm trying to figure out this formal proof. This is what I have so far but I'm stuck in trying to reach the goal. I'm not sure if what I did is correct so far since I'm still trying to learn this on ...
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, ...
71 views

474 views

### Formal deductions on Hilbert system

I have proved {(α→β),(β →γ)} ⊢ (α→γ) } using formal deductions using Modus Ponens and the three axiom of H2 : A1: A -> (B-> A) A2: (A-> (B->C)) -> ((A-> B) -> ( A -> C)) A3: (( ¬ A) -> ( ¬B)) -> ( ...
685 views

### What is a judgment?

I have a hard time trying to understand the concept of a judgment in natural deduction. One distinguishes between propositions and judgments. As I understand it, propositions are just well-formed ...
463 views

### Natural Deduction First Order Logic $∃y∀x(P(x) ∨ Q(y))↔∀x∃y(P(x) ∨ Q(y))$

I'm working on some of my logic exercises for my end term exam in Predicate Logic. One of these exercises is "Show with natural deduction that $\vdash ∃y∀x(P(x) ∨ Q(y))↔∀x∃y(P(x) ∨ Q(y))$" I'm ...
775 views

145 views

### Being a Mathematician [closed]

I love mathematics--the exploration of space and quantity and how areas of mathematics are interrelated. However, I think proofs of trivial theorems are boring and uninteresting. The more complex the ...
163 views

### Does the Definition of a Formal Proof in Mendelson's Book Allow for the Use of Theorem/Derived Axiom Schema in Formal Proofs?

The relevance of this question concerns deciding whether or not a sequence of well-formed formulas in a text will qualify as a formal proof. Mendelson's Introduction to Mathematical Logic on p. 25 of ...
93 views

### Deductive Logic : If A -> B it can be deduced neg(A) -> neg(B)

I am having a hard time proving the following $$(a \to b) \vdash (\lnot a \to \lnot b)$$ I followed the book advice and first proved that $(a \to b) \vdash (\lnot \lnot a \to \lnot \lnot b)$ ...
193 views

### Examples of non-trivial proofs in deductive systems

I want to get a better grasp of what a rigorous formal proof is. So I was hoping to find proofs of interesting results using natural deduction or Hilbert system or similar. The "interesting result" ...
48 views

### Why are these two lines not congruent (and other ways to figure out if other shapes are not congruent)

I stumbled apon this questions in a proofs worksheet and I was quite baffled by it because it seems like you can prove the sides to be congruent by cpctc however after I checked my work, the answers ...
2k views

### Prove that ${\sqrt 2}^{\sqrt 2}$ can be rational. [closed]

This is a question from Mathematics for Computer Science by Lehman: Prove that ${\sqrt 2}^{\sqrt 2}$ can be rational.Prove by making cases. How can we write it by showing different cases?
561 views

### Why are auxiliary lines valid in geometric proofs?

This probably seems like a super basic question, but I'm only on the level of an Honors Geometry course right now. Anyways, I don't understand why auxiliary lines are valid in proofs. Wouldn't they ...
39 views

### Does the Statement $\lim_{f(x)\to a}k(x)$ Make Sense

In a formal mathematics context does the statement $$\lim_{f(x)\to a}k(x)$$ where $f(x)\neq c$, where $c$ is a constant, make sense? For example does $$\lim_{x^2\to 0}x$$ make any sense in a formal ...
97 views

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
33 views

### How to use parentheses with one logical conective? [closed]

is (((a and b) and c) and d) equal to a and b and c without parentheses? Why?
124 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 \:...
265 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 ...
66 views

### How do I show the greatest lower bound for this set is 17?

Let $S = \{17 + \frac{1}{2n} : n \in \mathbb{N}\}$. Prove that the greatest lower bound of $S$ is $17$. What needs to be shown/proven? Thanks in advance.