tiva do ML não é adequada e só a teoria funciona.
Felizmente, só "trabalho" (brinco) com os modelos (infinito) categorias,
então mesmo se todo o construtivismo como enunciado na HoTT estiver
"errado" ainda tenho motivos para estudá-lo :)
Abs,
Fernando Yamauti
ity-in-Homotopy-Type-Theory-Part-I-The?redirectedFrom=fulltext
?> ?
Abs,
Fernando Yamauti
--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um
e-
Muito obrigado!
Em 3 de abril de 2017 13:28, Hermógenes Oliveira <
hermogenes.olive...@student.uni-tuebingen.de> escreveu:
> Fernando Yamauti <fgyama...@gmail.com> escreveu:
>
> > Oi,
> >
> > Será que alguém teria acesso ao paper
> >
> > 1 Lady
cia), com essa definição
se deriva ECQ. Não sei da onde tirei essa idéia maluca de que essa
definição seria correta.
Abs,
Fernando
Em 8 de abril de 2017 13:30, Fernando Yamauti <fgyama...@gmail.com>
escreveu:
> Oi Hermógenes
>
> > Não. A minha sugestão é diferente. \neg A d
m disso, ele introduz um tipo
'type' e termos 'i (A) : prop' para cada tipo A.
Portanto, de acordo com a sua afirmação, ML não estaria sendo
consistente?
Desculpe-me, mas ainda estou falhando em entender o que vai para o
espaço. Creio eu que você esteja pensando em um problema diferente do q
> tal como Martin-Löf faz, me parece um equívoco. Concordo ainda que a
> discussão epistemológica de Martin-Löf em conexão com a fundamentação
> da sua Teoria de Tipos é muito confusa, para se dizer o mínimo.
>
Brouwer não fazia a mesma coisa? Aquela idéia de matemático ideal
> compreender o tamanho da perda, é preciso apreciar o valor da distinção.
> Para isso, eu sugeri uma leitura atenta e *reflexiva* dos escritos mais
> *filosóficos* do Martin-Löf, com uma mente voltada para fundamentação.
> Não fornecerei uma explicação detalhada disso aqui na lista
Em 3 de julho de 2017 09:40, jyb escreveu:
> Gostaria de apontar que o Saul Kripke apresentou em Paris uma prova
> semantica do teroema de Gödel
> "A Model Theoretic Approach to Gödel's Theorem"
> http://www.logic-in-question.org/
> Bem detalhada mas ainda não publicada,
Olá a todos,
Primeiramente, só queria levantar dois pontos.
1) Eu, como havia comentado aqui ou na HoTT Café (não me lembro ao certo),
também achava que \neg \neg G somente poderia ser considerada verdadeira,
mas fui chamado a atenção (pelo Matt Oliveri) de que G já é
construtivamente
Baixa o pacote inteiro do MacTeX http://www.tug.org/mactex/
PS: O MacTeX contem o TeXShop entre outros editores e mais alguns
programas muito úteis (tipo BibDesk e LaTeXiT)
Em 7 de agosto de 2017 15:41, Famadoria escreveu:
> TeXShop.
>
> Sent from my iPhone
>
> On 7 Aug
As referências em https://ncatlab.org/nlab/show/pure+type+system caso
busque o mais geral possível. Para algo mais básico, acho melhor começar
com untyped lambda cálculo, algo como em
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf
ou no livro do Barendregt, e entender
ative
>extension of intuitionistic logic with a new connector (subtraction) dual
>to implication. Eventually, we consider first order subtractive logic and
>we present an embedding of classical logic into subtractive logic.
>
> abs
> Valeria
>
> 2017-10-25 3:21
Oi Chico,
Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
vale em qualquer topos Booleano, mas mesmo em Set algo do tipo (-) \vee A
-| (-) \Delta A (ou o contrario), onde ambos endofuntores são entre
Só duas consideração provavelmente irrelevantes e que não interessam a
ninguem. Na pratica matemática, se prova a negação de algo assumindo esse
algo e chegando a uma contradição. Mas do ponto de vista do significado da
proposição \neg A, ele é completamente determinado pela regra de introdução
Uma prova canônica é uma prova direta ou imediata. Mais precisamente, uma
prova canônica é qualquer termo dado por uma única aplicação de uma unica
regra de introdução à qualquer termos, canônicos ou não. Essa definição
difere da noção de forma canonica (termos dados somente por regras de
Estou tentando evitar procrastinar, mas não consigo resistir em comentar
sobre isso.
"Marx and Engels, and their Marxist successors, thought that the analysis
> of variation would require the creation of a dialectical logic or a “logic
> of contradiction”. But traditional logic survived in
16 matches
Mail list logo