Re: [Logica-l] Gödel vitima da Reductio ad Paternum?

2013-06-12 Por tôpico Rodrigo Freire 
Muito oportunos os pontos levantados pelo Jean Yves e os comentários
do João Marcos.

Acho que Godel e Turing são os lógicos mais celebrados do século XX, e
certamente são grandes pensadores. Compará-los com outros lógicos que
fizeram trabalhos similares não diminui em nada a grandeza desses
pensadores, e fazer isso pode ser muito útil. Estou aprendendo muita
coisa com essa discussão aqui na lista.

Interessante que o Post, em certo sentido, antecipou muitos dos
principais resultados do Godel
e do Turing (e Church), e fez muitas outras coisas, mas não é
celebrado como esses dois. Acho que é esclarecedor entender as
diferenças. Muitos livros de computabilidade adotam o enfoque de Post
para as máquinas de Turing. O livro do Mal'cev utiliza a expressão
"máquina de Turing-Post", no começo, e depois fica com a expressão
mais standard (e mais curta) "máquina de Turing".

O artigo da Lisbeth de Mol, mencionado aqui pelo Jean Yves, analisa a
diferença entre os métodos de Post e de Godel. O artigo do Soare,
indicado pelo Ruy de Queiroz mostra em que as análises do Turing foram
além das de Post. Acho que esses trabalhos contribuem muito para a
compreensão das origens da computabilidade.


Abraço
Rodrigo



2013/6/11 Joao Marcos :
>> O  teorema de incompletude de Gödel depende de muitas coisas que o Gödel
>> nao inventou:
> [...]
>> - paradoxo do mentiroso (Gödel falou explictamente que ele se inspirou
>> deste paradoxo)
>
> A despeito do que o próprio Gödel terá dito informalmente acerca de
> sua fonte de inspiração, o que importa neste caso parece ser o uso do
> procedimento de diagonalização inventado (?) por Cantor.
>
> Não podemos deixar de apontar a séria confusão que está em comparar o
> primeiro teorema de incompletabilidade de Gödel ao Paradoxo do
> Mentiroso: Gödel *não* demonstrou que há "verdades que não são
> verdadeiras", na Aritmética, mas que há ali *verdades que não são
> demonstráveis por uma teoria recursivamente axiomatizável*.
> Wittgenstein morreu sem entender isso.
>
>> Gödel por causa da excentricidade dele virou uma lenda.
>> Do outro lado poucas pessoas falam do Paul Bernays
>> que era uma pessoa  discreta
>> que fiz contribucoes muito importante a logica,
>> e que foi uma das pessoas mas proxima ao Gödel,
>> Ver o artigo do Feferman:
>> http://math.stanford.edu/~feferman/papers/bernays.pdf
>
> O trabalho do discreto Bernays foi de fato simplesmente sensacional, e
> sem ele personalidades díspares como Hilbert e Fraenkel teriam ambos
> produzido cientificamente substancialmente menos do que de fato
> produziram.  Se Bernays não tivesse tido este papel, contudo, ainda
> assim teria entrado para a história como o orientador do Gentzen.  Ou
> será que agora estou "idolatrando" esse tal de Gentzen?
>
> Joao Marcos
>
> --
> http://sequiturquodlibet.googlepages.com/
> ___
> Logica-l mailing list
> Logica-l@dimap.ufrn.br
> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] Gentzen vitima da Reductio ad Paternum?

2013-06-12 Por tôpico jean-yves beziau 
>
>
> O trabalho do discreto Bernays foi de fato simplesmente sensacional, e
> sem ele personalidades díspares como Hilbert e Fraenkel teriam ambos
> produzido cientificamente substancialmente menos do que de fato
> produziram.  Se Bernays não tivesse tido este papel, contudo, ainda
> assim teria entrado para a história como o orientador do Gentzen.  Ou
> será que agora estou "idolatrando" esse tal de Gentzen?
>
> Joao Marcos
>
>
E facil aplicar a Reductio ad Paternum ao Gentzen
ele seria o *pai* da teoria de prova
e aplicando a Reduction ad Avum
o Hilbert seria o avo da teoria de prova - ele inventou a expressao e o
conceito
(Beweistheorie sinonima para ele de Metamatematik)
Isso seria deixar de lado o Bernays que de fato foi oficialemente o
orientador do Gentzen
mas que tive um papel que nao se limitou a um papel adminsitrativo
Talvez podemos aplicar a Reductio ao Tium = Bernays seria o *tio* da teoria
da prova.

O Bernays orientou tambem o trabalho do Paul Hertz na base do qual o
Gentzen comecou a trabalhar.
O Satzsysteme de Hertz e claramente um primeiro passo para sistemas de
sequentes a la Gentzen.
O trabalho do Hertz ainda e pouco conhecido.
Foi publicado em ingles pela primeira vez na nossa antologia de logica
universal,
apresentado pelo Javier Legris, um dos melhores especialistos do Hertz
http://www.springer.com/birkhauser/mathematics/book/978-3-0346-0144-3

Essa antologia se chama:
Universal Logic: An Anthology - From Paul Hertz to Dov Gabbay
Mas quero enfatizar que escolhendo este titulo
nao quiz fazer mais uma vitima da Reductio ad Paternum
dizendo que o Hertz e o *pai* da logica universal.

JYB
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] Gödel = uma super maquina de Turing?

2013-06-12 Por tôpico jean-yves beziau 
Com se sabe logo depois do segundo teorema de incompletude do Gödel
Gentzen provou a consistencia (relativa) da aritmetica.

Gödel gostava muito do trabalho do Gentzen e passou anos estudando este
trabalho
o que levou ele ao ultimo resultado importante dele, sua prova "dialectica"
que se chama assim porque foi publicado no jornal Dialectica na decada 50.
(journal Suiço fundado por Bernays, Bachelard e Gonseth).

Este exemplo mostra mais uma vez que o Gödel foi mas um provador
(talvez um tipo de  super maquina de Turing) que um conceptualizador.

JYB
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] Turing e Post

2013-06-12 Por tôpico Famadoria 
Alguem comentou o trabalho de Turing de 1939 sobre sequências de teorias? Foi 
seu doutorado, creio. 

Sent from my iPhone

On 11/06/2013, at 21:45, Ruy de Queiroz  wrote:

> Caro Rodrigo,
> 
> Vale a pena prestar atenção ao que diz o artigo
> 
> Turing Oracle Machines, Online Computing, and Three Displacements in
> Computability 
> Theory
> Robert I. Soare
> 
> 
> sobretudo no que concerne a algumas referências à opinião de Gödel (em
> 1955) sobre as contribuições de Turing:
> 
> “When I first published my paper about undecidable propositions the result
> could not be pronounced in this generality, because for the notions of
> mechanical procedure and of formal system no mathematically satisfactory
> definition had been given at that time. ...
> The essential point is to define what a procedure is.”
> “That this really is the correct definition of mechanical computability was
> established beyond any doubt by Turing.”
> 
> 
> 
> Johan von Neumann é outro que se rende à originalidade de Turing, sobretudo
> no que diz respeito à noção de "máquina/autômato universal":
> 
> “An automaton is “universal” if any sequence that can be produced by any
> automaton whatsoever can also be produced by this automaton.”
> “Turing observed that a completely general description of any conceivable
> automaton can be  (in the sense of the above definition) given in a finite
> number of words.”
> (“The General and Logical Theory of
> Automata”,
> Setembro 1948)
> 
> 
> 
> Sobre a noção de máquina universal, Martin Davis diz:
> 
> “People had been thinking about calculating machines for a long time, since
> Leibniz’s time and even earlier.
> Before Turing the general supposition was that in dealing with such
> machines the three categories, machine, program, and data, were entirely
> separate entities. The machine was a physical object; today we would call
> it hardware. The program was the plan for doing a computation, perhaps
> embodied in punched cards or connections of cables in a plugboard. Finally,
> the data was the numerical input.
> Turing’s universal machine showed that the distinctness of these three
> categories is an illusion"
> 
> The Universal 
> Computer(2000)
> 
> 
> 
> Resolver negativamente o Entscheidungsproblem  de Hilbert através de um
> modelo razoavelmente intuitivo de máquina/algoritmo não foi pouca coisa,
> principalmente para o próprio desenvolvimento da Lógica Matemática.
> 
> Abraço,
> Ruy
> 
> 
> 
> Em 11 de junho de 2013 21:11, Rodrigo Freire escreveu:
> 
>> Caros
>> 
>> Ótimas respostas.
>> 
>> Alguns comentários e questões:
>> 
>> 1- Walter: Pelo que me lembro, o livro de computabilidade adota o
>> enfoque de Post para as máquinas de Turing, segundo o qual uma máquina
>> de Turing é um conjunto finito de quadruplas, e não de quintuplas como
>> fez o Turing?
>> 
>> 2- O livro do Martin Davis, computability and unsolvability adota o
>> enfoque de Post para máquinas de Turing. (página 5).
>> 
>> 3- O Marcelo Finger respondeu muito bem sobre as motivações políticas
>> em torno desse fenômeno de homenagens ao Turing.
>> 
>> 4- O Jean Yves já respondeu a Valeria, mas o Martin Davis é de fato
>> uma espécie de filho intelectual do Post.
>> 
>> 5- Entendo que a homenagem ao Turing é uma homenagem à Lógica através
>> de uma figura que tem apelo fora do meio restrito de lógicos. Mas acho
>> que há alguns exageros. Por exemplo, por que a capa do recém criado
>> journal "Computability" é uma imagem do Turing? Em que isso homenageia
>> a lógica? Olhando para os conteúdos já publicados nesse journal, vejo
>> que são artigos de computabilidade comparáveis aos que aparecem em
>> outras revistas de lógica, e nada especialmente ligado ao Turing.
>> 
>> 6- Enfim, me parece que o Post deveria ser considerado o "father of
>> computer science" e não o Turing, como afirma o Barry Cooper.
>> Certamente há pessoas na lista muito mais qualificadas que eu para
>> fazer esse tipo de julgamento e eu gostaria de ouvir a opinião dos
>> membros da lista sobre isso.
>> 
>> Abraço
>> Rodrigo
>> ___
>> Logica-l mailing list
>> Logica-l@dimap.ufrn.br
>> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
> ___
> Logica-l mailing list
> Logica-l@dimap.ufrn.br
> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] Turing e Post

2013-06-12 Por tôpico Marcelo Finger 
Na minha modesta opinião, melhor um Turing homenageado do que nem
Turing nem Post.

2013/6/12 Famadoria :
> Alguem comentou o trabalho de Turing de 1939 sobre sequências de teorias? Foi 
> seu doutorado, creio.
>
> Sent from my iPhone
>
> On 11/06/2013, at 21:45, Ruy de Queiroz  wrote:
>
>> Caro Rodrigo,
>>
>> Vale a pena prestar atenção ao que diz o artigo
>>
>> Turing Oracle Machines, Online Computing, and Three Displacements in
>> Computability 
>> Theory
>> Robert I. Soare
>>
>>
>> sobretudo no que concerne a algumas referências à opinião de Gödel (em
>> 1955) sobre as contribuições de Turing:
>>
>> “When I first published my paper about undecidable propositions the result
>> could not be pronounced in this generality, because for the notions of
>> mechanical procedure and of formal system no mathematically satisfactory
>> definition had been given at that time. ...
>> The essential point is to define what a procedure is.”
>> “That this really is the correct definition of mechanical computability was
>> established beyond any doubt by Turing.”
>>
>>
>>
>> Johan von Neumann é outro que se rende à originalidade de Turing, sobretudo
>> no que diz respeito à noção de "máquina/autômato universal":
>>
>> “An automaton is “universal” if any sequence that can be produced by any
>> automaton whatsoever can also be produced by this automaton.”
>> “Turing observed that a completely general description of any conceivable
>> automaton can be  (in the sense of the above definition) given in a finite
>> number of words.”
>> (“The General and Logical Theory of
>> Automata”,
>> Setembro 1948)
>>
>>
>>
>> Sobre a noção de máquina universal, Martin Davis diz:
>>
>> “People had been thinking about calculating machines for a long time, since
>> Leibniz’s time and even earlier.
>> Before Turing the general supposition was that in dealing with such
>> machines the three categories, machine, program, and data, were entirely
>> separate entities. The machine was a physical object; today we would call
>> it hardware. The program was the plan for doing a computation, perhaps
>> embodied in punched cards or connections of cables in a plugboard. Finally,
>> the data was the numerical input.
>> Turing’s universal machine showed that the distinctness of these three
>> categories is an illusion"
>>
>> The Universal 
>> Computer(2000)
>>
>>
>>
>> Resolver negativamente o Entscheidungsproblem  de Hilbert através de um
>> modelo razoavelmente intuitivo de máquina/algoritmo não foi pouca coisa,
>> principalmente para o próprio desenvolvimento da Lógica Matemática.
>>
>> Abraço,
>> Ruy
>>
>>
>>
>> Em 11 de junho de 2013 21:11, Rodrigo Freire escreveu:
>>
>>> Caros
>>>
>>> Ótimas respostas.
>>>
>>> Alguns comentários e questões:
>>>
>>> 1- Walter: Pelo que me lembro, o livro de computabilidade adota o
>>> enfoque de Post para as máquinas de Turing, segundo o qual uma máquina
>>> de Turing é um conjunto finito de quadruplas, e não de quintuplas como
>>> fez o Turing?
>>>
>>> 2- O livro do Martin Davis, computability and unsolvability adota o
>>> enfoque de Post para máquinas de Turing. (página 5).
>>>
>>> 3- O Marcelo Finger respondeu muito bem sobre as motivações políticas
>>> em torno desse fenômeno de homenagens ao Turing.
>>>
>>> 4- O Jean Yves já respondeu a Valeria, mas o Martin Davis é de fato
>>> uma espécie de filho intelectual do Post.
>>>
>>> 5- Entendo que a homenagem ao Turing é uma homenagem à Lógica através
>>> de uma figura que tem apelo fora do meio restrito de lógicos. Mas acho
>>> que há alguns exageros. Por exemplo, por que a capa do recém criado
>>> journal "Computability" é uma imagem do Turing? Em que isso homenageia
>>> a lógica? Olhando para os conteúdos já publicados nesse journal, vejo
>>> que são artigos de computabilidade comparáveis aos que aparecem em
>>> outras revistas de lógica, e nada especialmente ligado ao Turing.
>>>
>>> 6- Enfim, me parece que o Post deveria ser considerado o "father of
>>> computer science" e não o Turing, como afirma o Barry Cooper.
>>> Certamente há pessoas na lista muito mais qualificadas que eu para
>>> fazer esse tipo de julgamento e eu gostaria de ouvir a opinião dos
>>> membros da lista sobre isso.
>>>
>>> Abraço
>>> Rodrigo
>>> ___
>>> Logica-l mailing list
>>> Logica-l@dimap.ufrn.br
>>> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
>> ___
>> Logica-l mailing list
>> Logica-l@dimap.ufrn.br
>> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
> ___
> Logica-l mailing list
> Logica-l@dimap.ufrn.br
> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l



-- 
Marcelo Finger
Department of Computer Science, Cornell Univ

[Logica-l] formalização dos teoremas de incompletude em Isabelle

2013-06-12 Por tôpico Joao Marcos 
"The full development is concise, at under 17,000 lines, plus a
further 3000 lines to develop HF set theory."

JM


-- Forwarded message --
Date: Wed, 12 Jun 2013 12:37:10 -0400
From: Jeremy Avigad 
Subject: incompleteness theorems formally verified


Dear friends and colleagues,

Larry Paulson, Professor of Computational Logic at Cambridge University,
has recently completed a formal verification of G?del's incompleteness
theorems, using the popular Isabelle interactive proof system.

Because this should be of interest to the FOM community, I asked him to
send me an announcement that I could post to this list. That
announcement appears below.

Paulson was the initial designer of Isabelle, which he continues to
develop with Tobias Nipkow and Makarius Wenzel. About 10 years ago, he
also formalized G?del's constructible hierarchy in Isabelle, to prove
the relative consistency of the axiom of choice. Related publications
can be found on his web page,

http://www.cl.cam.ac.uk/~lp15/ 

Best wishes,

Jeremy Avigad

**

Larry's announcement:

I've completed a formalisation of G?del's two incompleteness theorems,
including what may be the first-ever formalisation of the second
incompleteness theorem. The proof was done in Isabelle/HOL and uses
Christian Urban's Nominal2 package for dealing with bound variables. The
formalisation follows an unpublished paper by S S'wierczkowski, who
presents proofs of both incompleteness theorems using the hereditarily
finite sets rather than Peano Arithmetic:

http://journals.impan.gov.pl/dm/PDF/dm422-0-00.pdf

Proving the second incompleteness theorem requires some quite intricate
operations on alphabets, as well as lengthy derivations in an internal
calculus. Apart from those derivations, the proof script is structured
and quite legible. The full development is concise, at under 17,000
lines, plus a further 3000 lines to develop HF set theory. (A recent Coq
proof of the first incompleteness theorem alone is over 52,000 lines.)

The development is instructive. While first-order logic is formalised
here using "nominal" binding primitives, the coding uses de Bruijn
indexes. A precise correspondence is proved between the two
representations of formulas. A series of correspondence proofs provides
confidence in the correctness of the complicated syntactic definitions.
The second incompleteness theorem follows from the Hilbert-Bernays
derivability conditions. Proving the crucial theorem |- A IMP
Provable["A"] requires transforming a coded formula. During this
process, the coded variables (which are constant terms) need to be
replaced by terms consisting of a special function applied to the same
variable (not coded). But this calculus has no functions, and this step
needs to be expressed by introducing new variables that satisfy a
certain relation with the original variables. The proof is by induction
on the formula A, but relies on properties proved by a mutual induction
within the encoded first-order calculus itself.
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] Reductio ad Disjunctum

2013-06-12 Por tôpico jean-yves beziau 
Concordo plenamento com seu raciocino Marcelo
e na mesma linha de Reductio ad Disjunctum diria
Melhor um  Ratinho ser homenageado que nem o Ratinho nem o Faustao ser
homenageado !
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] 2nd Announcement: Conference in honour of Ofelia Alas - Brazilian Conference on General Topology and Set Theory - STW 2013

2013-06-12 Por tôpico samuel 

 Sorry for duplicate messages **


Dear Colleagues,

This is the second announcement for the Brazilian Conference on
General Topology and Set Theory – STW 2013, in honour of Ofelia Alas
on the occasion of her 70th birthday.

The conference will take place from 12th to 16th August 2013 at the
Beach Hotel Maresias, Sao Sebastiao, Brazil
(http://www.maresiashotel.com./br), on the coast of the state of Sao
Paulo, about 200 km from the city of Sao Paulo.

The conference will be dedicated to all branches of General Topology,
Set Theory and their applications and will consist of 9 plenary talks,
2 minicourses, contributed talks of 25 minutes and poster sessions.

A special issue of Topology and its Applications will be dedicated to
the proceedings of the conference.

Invited speakers:

- Angelo Bella
- Carlos Di Prisco
- Salvador Garcia-Ferreira
- Istvan Juhasz
- Manuel Sanchis
- Franklin D. Tall
- Angel Tamariz-Mascarua
- Mikhail Tkachenko
- Richard G. Wilson

Minicourses:

- Christina Brech
- Ramiro de la Vega

A list of accepted talks can be seen at
http://at.yorku.ca/cgi-bin/abstract/cbgl-01

Conference webpage: http://www.ime.usp.br/~lucia/stw2013

E-mail: stw2013saopa...@gmail.com

Organizers:
- Lucia R. Junqueira, chair (Universidade de Sao Paulo, USP)
- Leandro F. Aurichi (USP)
- Rodrigo R. Dias (USP)
- Marcelo D. Passos (Universidade Federal da Bahia, UFBA)
- Samuel G. da Silva (UFBA)

Deadline for pre-registration and abstracts: July 1, 2013.

Please check website for further information.

*


Universidade Federal da Bahia - http://www.portal.ufba.br

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l