Talk:Disjunction and existence properties

From Wikipedia, the free encyclopedia

Mathematics Portal

This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.

Mathematics rating:

Stub Class

Low Priority

Field: Foundations, logic, and set theory

Please update this rating as the article progresses, or if the rating is inaccurate. Click to show/hide comments.
Please add to or update the comments to suggest improvements to the article.
Geometry guy 16:26, 10 June 2007 (UTC)

To-do list for Disjunction and existence properties:	edit · history · watch · refresh
From 24-Sep-2004: Discussion of Herbrand's theorem Discussion of Brouwer-Heyting-Kolmogorov interpretation Discussion of axiom of choice CM's number theoretic conjecture New: Bit about indecomposible project object requires explanation

To-do list for Disjunction and existence properties:

edit · history · watch · refresh

From 24-Sep-2004:

Discussion of Herbrand's theorem
Discussion of Brouwer-Heyting-Kolmogorov interpretation
Discussion of axiom of choice
CM's number theoretic conjecture

New:

Bit about indecomposible project object requires explanation

1 Charles matthew's number theoretic conjecture
2 A quibble
3 Examples
4 The formulas must be sentences

[edit] Charles matthew's number theoretic conjecture

The number theory example I'm thinking of is a quite striking one about primitive roots. Charles Matthews 19:30, 23 Sep 2004 (UTC)

[edit] A quibble

In particular the existence property is fundamental to understanding in what sense proofs can be considered to have content: the essence of the discussion of existence theorems.

Herbrand's theorem, in its original form and for many classical theories, tells us something weaker than the existence property; namely it tells us that for some t1 ... tn, phi(t1) \/ ... \/ phi(tn) is a theorem, so any model must identify which of those ti is the (a) witness. I think Herbrand's theorem does establish that the proof has content, in the sense you describe, for non-constructive theories. Oh, and I'd like to hear more about your number theoretic example. ---- Charles Stewart 11:37, 24 Sep 2004 (UTC)

So, it would be good to have discussion of the proof theory : both Herbrand's theorem, and also the argument that in a cut-free proof with last line proving a disjunction, the penultimate line must prove a disjunct (sorry if I'm putting this badly - my knowledge of the field is a bit amateurish). Primitive roots - I'm thinking of the approximation to the Artin conjecture which says that, at least one out of 2, 3, 5 is a primitive root modulo infinitely many primes: but we can't know which. I have thought for a while that a logician's commentary on this would be interesting, and less hackneyed than some of the other examples of non-constructive techniques and possible 'proof unwinding'. Charles Matthews 12:46, 24 Sep 2004 (UTC)

also the argument that in a cut-free proof with last line proving a disjunction, the penultimate line must prove a disjunct

In fact this isn't a theorem (I assumke you're talking about the sequent calculus): in LK the last rule applied can be a contraction, which is why the disjunction property can't be proven for LK;

at least one out of 2, 3, 5 is a primitive root modulo infinitely many primes: but we can't know which.

I don't know the conjecture (I've heard of the Artin conjecture, but I can't recall what it's about, should read more wikipedia, I guess), but it looks like this would be an excellent addition to the page ---- Charles Stewart 16:49, 24 Sep 2004 (UTC)

According to the article Artin's conjecture on primitive roots, the candidates are {3, 5, 7}. It says the proof is non-constructive, fine... but you claim, "we can't know which", and I can't tell if you mean to say that Heath-Brown somehow proved that it's undecidable (?) or if it's simply unknown as yet. --Jorend 20:10, 29 November 2006 (UTC)

[edit] Examples

From the article:

There are quite concrete examples in number theory where this has a major effect.

I think it would be helpful to give two or so examples of this. CRGreathouse (t | c) 23:27, 7 February 2007 (UTC)

[edit] The formulas must be sentences

I added the word "sentence" (closed formula) to the disjunction property and to the existence property. About the disjunction property, I think that it doesn't hold (at least in some versions of) Heyting arithmetic if the formula $\phi \vee \psi$ isn't closed: for example, (a version of) Heyting arithmetic proves $x = 0 \vee x \neq 0$ but doesn't prove $x = 0$ and doesn't prove $x \neq 0$ . About the existence property, I think that is just a matter of convention to assume that the formula $\exists x\colon \phi(x)$ is closed. (I'm assuming that the term theorem doen't imply that the formula is closed — I hope that I got this right). Jayme 15:44, 9 August 2007 (UTC)