Talk:Disjunction and existence properties

From Wikipedia, the free encyclopedia

You have new messages (last change).

	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

[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)