Oi lista,
Seja s:=sqrt(2).
Sabemos que s é irracional, e que
(s^s)^s = s^(s*s) = s^2 = 2,
e 2 é racional.
Notação: Irr(s), Rat((s^s)^s).
Quero entender onde é que a prova clássica para
Ex a,b. Irr(a) & Irr(b) & Rat(a^b)
dá problema quando a interpreto intuicionisticamente.
Vamos usar b:=s, então essa sentença simplifica:
Ex a. Irr(a) & Rat(a^s).
Então:
Irr(s^s) => (Irr(s^s) & Rat((s^s)^s)) => (Ex a. Irr(a) & Rat(a^s))
Rat(s^s) => (Irr(s) & Rat(s^s)) => (Ex a. Irr(a) & Rat(a^s))
Daí posso deduzir que:
(Irr(s^s) \/ Rat(s^s)) => (Ex a. Irr(a) & Rat(a^s))
Até agora todos os passos são válidos intuicionisticamente...
Mas eu sou um intuicionista não-isolacionista, e eu sei pra eu
conseguir dialogar com os meus coleguinhas matemáticos clássicos eu às
vezes tenho que mostrar "modelos" pra determinados sistemas
intuicionistas pra convencê-los de que certas sentenças não são
deriváveis intuicionisticamente - porque as sentenças que são
deriváveis são verdadeiras em todos os modelos, blablablá - é, eu sei
que intuicionistas "de verdade" não precisam de modelos, mas sabe como
é, é que os matemáticos clássicos acham argumentos via Teoria da Prova
muito esquisitos, e não têm paciência pra acompanhá-los...
Alguém sabe me mostrar um contra-modelo para
(Irr(s^s) \/ Rat(s^s)) => (Ex a. Irr(a) & Rat(a^s)),
onde o valor de verdade dessa sentença seja mais fraco que
"verdadeiro"? Eu sei que a dupla negação dela vai ser verdadeira...
Eu tenho a impressão - deixa eu fazer um paralelo com Análise
Não-Standard - de que em qualquer modelo para Geometria Diferencial
Sintética a fórmula "Irr(s^s) \/ Rat(s^s)" é "standard", já que ela
não tem variáveis livres, então posso usar o "teorema de
transferência", e com isso descubro que ela é "verdadeira"... e isso
implicaria em
Ex a. Irr(a) & Rat(a^s) -
mas não tenho como conferir isso agora - meus livros de SDG estão
todos emprestados, e de qualquer modo eu não entendo as construções
bem, e só estou aprendendo feixes direito agora... 8-\
Comentários?
[],
Eduardo Ochs
[EMAIL PROTECTED]
http://angg.twu.net/
_______________________________________________
Logica-l mailing list
[email protected]
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
