Re: [Logica-l] em um mundo sem terceiras opções...

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

Re: [Logica-l] Re: sobre a "melhor forma" de apresentar a negação em lógicas construtivas

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

Re: [Logica-l] Dúvidas sobre Dummett

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

Re: [Logica-l] Textos introdutórios sobre Teoria de Tipos

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

Re: [Logica-l] um probleminha com logica intuicionista...

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

Re: [Logica-l] um probleminha com logica intuicionista...

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

Re: [Logica-l] LaTeX para Mac

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

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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,

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

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

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

> 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

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

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

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

> 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

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

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

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

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

[Logica-l] Philosophia Mathematica Vol 23 Issue 3

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-