# Tag Info

2

The right way to build such a category is a philosophical question. There are different approaches in the mathematical literature. One thing is clear though: the objects should be propositions, not just theorems. The problem is to define equality of proofs in a sensible way. For example, let $\Pi$ be Pythagoras' theorem. Should each of the over 100 proofs ...

3

See for example Lambek and Scott: Introduction to higher order categorical logic, ch 0.1 (unfortunately not in the net but for sure in ur university library). There first is defined a graph, then a deductive system as a graph with For each object $A$ an identity arrow $1_A:A\rightarrow A$ For each pair of arrows $f:A\rightarrow B$ and $g:B\rightarrow C$ ...

5

This paper, called Physics, Topology, Logic and Computation: A Rosetta Stone does just that in section 3.2. If you have time and interest, I would suggest reading the entire paper (since the whole thing is pretty cool).

3

There is an important issue with statements of the form "$X$ is unprovable": in what system is $X$ unprovable? We assume here that $X$ is some consistent statement written in some formal language. Statements provable with no non-logical axioms are known as logical validities. Few interesting mathematical statements are phrased as logical validities. So the ...

0

If a conjecture X is unprovable that can be translated to the following: if X is true no contradiction can be derived if X is false no contradiction can be derived Both of these must be true because otherwise X would not be unprovable (we could merely choose one of the appropriate routes and eventually find a contradiction) That being said it becomes ...

1

A proof consists of a sequence of statements. When are two sequences distinct? Well, if two sequences have a different length, then they qualify as distinct. Now consider any proof that you have which say proves A as an intermediate step before you prove the conclusion C. Well, since A is true, it follows that (B$\rightarrow$A) holds as true also (where ...

1

The inequalities are preserved because $t$ and $(1-t)$ are positive: $$tAx\leq tb$$ $$(1-t)Ay \leq (1-t)b$$ So: $$A(tx+(1-t)y)=tAx + (1-t)Ay\leq tb + (1-t)b = b$$

1

Hint. Rewrite $t(ax-ay) + ay$ as $(1-t)ay + tax$, now use $1-t, t \ge 0$ and $ax, ay \le b$.

2

Coq seems to be happy with this. The easy direction (sigT is $\Sigma$ and forall is $\Pi$): Parameter V : Type -> Type. Lemma rabbit : sigT V -> forall Y, (forall X , V X -> Y) -> Y. Proof. firstorder. Qed. Print rabbit. We get the following proof: fun (X : sigT V) (Y : Type) (P : (forall Z : Type, V Z -> Y)) => sigT_rect ...

1

For second-order logic with Natural Deduction, you can see : Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965) or : Dirk van Dalen, Logic and Structure (5th ed - 2013). Both prove : $ΣX.V \equiv ΠY.(ΠX.(V→Y))→Y$. See van Dalen, page 150, Theorem 5.5 (e) : $\vdash_2 ∃X^n \varphi ↔ ∀X^0(∀X^n((\varphi → X^0) ... 0 The equation$\bf f(n)= n^2-12n + 35$is a quadratic equation in$\bf n$, Discriminant of which is$\bf D=\sqrt{12^2-4.35}=2$which is positive and thus there must exist two distinct roots of it which are$\bf 5$and$\bf 7$[remember$\alpha,\beta=\{12\pm\sqrt{4}\}/2$from quadratic formula];Since it is a parabola facing upwards it must have negative values ... 2 To prove that the statement: $$\forall n\in\Bbb N,\quad n^2-12n+35\ge0$$ isn't true it suffices to show that its negation: $$\exists n_0\in\Bbb N,\quad n_0^2-12n_0+35<0$$ is true and your choice$n_0=6$does the job. 0 Well if the sum of a rational and an irrational number is rational, then you could have something like your example, x=p/q-a/b, and we already know that irrational numbers can't equal rational numbers. 1 In general,$b\ge 2a\Rightarrow b^2\ge 4a^2$is not true. It's true if$b\ge 2a\ge 0.$You can do with$b\ge 2|a|$as the followings : Since$b\ge 2|a|\ge 0$, we have$b+2|a|\ge 0$and$b-2|a|\ge 0$. Then by the proposition, we have $$\frac{(b+2|a|)+(b-2|a|)}{2}\ge\sqrt{(b+2|a|)(b-2|a|)}\iff b\ge\sqrt {b^2-4a^2}$$ as desired. Here, note that$|a|^2=a^2$. 4 Sequent proofs should tend to write themselves without you having to think about them (which is the the point of using them!). The motto is: start from where you want to end up and work backwards (or rather upwards: in other words, write the sequent you want to prove at the bottom, and construct the tree from bottom to top ...). You want to establish the ... 1 A "long" comment. You can use this example to "format" the sequent calculus axiom and rules : $${ \quad \over \Gamma, A \implies A, \Delta } \, \text{(Axiom)}$$ $${ \Gamma \implies A \quad B \implies \Delta \over \Gamma \implies A \rightarrow B, \Delta } \, \text{(Rule)}$$ 2 What you've called "rule" is usually called "axiom" or "axiom scheme" and "identities" are usually called "rules".$A \Rightarrow A, B, C$(axiom) and$A, B \Rightarrow B, C$(axiom) implies$A, A\rightarrow B \Rightarrow B, C$by the second rule. 1 and$A, A\rightarrow B, C \Rightarrow C$(axiom) implies$A, A\rightarrow B, B\rightarrow C \Rightarrow C\$ ...

Top 50 recent answers are included