Perguntas sobre a análise de provas em teorias
Vou recapitular as anotações do curso no CIS 500: Software Foundations e os exercícios são muito divertidos. Estou apenas no terceiro exercício, mas gostaria de saber mais sobre o que está acontecendo quando uso táticas para provar coisas comoforall (n m : nat), n + n = m + m -> n =...
Esta é uma pergunta de acompanhamento para Qual é a diferença entre provas e programas (ou entre proposições e tipos)? O programa que corresponderia a uma prova não-construtiva (clássica) do formulário ∀ K t ( E , K ) ∨ ¬ ∀ K t ( e , k )∀k T(e,k)∨¬∀k T(e,k)\forall k \ T(e,k) \lor \lnot \forall k...
Estou procurando criar notações para grandes ordinais contáveis de uma "maneira natural". Por "caminho natural", quero dizer que, dado um tipo de dados indutivo X, essa igualdade deve ser a igualdade recursiva usual (a mesma que deriving Eqem Haskell produziria) e a ordem deve ser a ordem...
Eu tenho lido muito sobre sistemas de tipos e coisas desse tipo e entendo por que eles foram introduzidos (para resolver o paradoxo de Russel). Eu também entendo aproximadamente sua relevância prática em linguagens de programação e sistemas de prova. No entanto, não estou totalmente confiante de...
Em um tópico recente na lista de discussão da Agda, surgiu a questão das leis ηη\eta , na qual Peter Hancock fez comentários instigantes . Meu entendimento é que leis vêm com tipos negativos, ie. conectivos cujas regras de introdução são invertíveis. Para desabilitar para funções, Hank sugere o...
Normalização fraca para o cálculo lambda de tipo simples pode ser comprovada (Turing) por indução em . Um cálculo lambda estendido com recursores em números naturais (Gentzen) possui uma estratégia de normalização fraca por indução em .ω2ω2\omega^2ϵ0ϵ0\epsilon_0 E o Sistema F (ou mais fraco)?...
Há pouco tempo, alguém primeiro me disse que call / cc podia permitir objetos de prova para provas clássicas, implementando a lei de Peirce. Eu pensei um pouco sobre o assunto recentemente e não consigo encontrar uma falha nele. No entanto, eu realmente não consigo ver mais ninguém falando sobre...
Eu estou procurando artigos e artigos sobre lógicas estruturais subestruturais - não sobre a semântica de modalidades lógicas lineares, mas sobre lógicas subestruturais aumentadas com operadores modais padrão, por exemplo, K estrutural (algo como MALL com operador de caixa, necessidade e regras...
Esta pergunta é sobre lógica proposicional e todas as ocorrências de "resolução" devem ser lidas como "resolução proposicional". Essa questão é extremamente básica, mas está me incomodando há algum tempo. Vejo pessoas afirmarem que a resolução proposicional está completa, mas também vejo pessoas...
Para uma teoria de tipos, por consistência, quero dizer que ela tem um tipo que não é habitado. Da forte normalização do cubo lambda, segue-se que o sistema FFF e o sistema FωFωF_\omega são consistentes. Os tipos indutivos de MLTT + também têm uma prova de normalização. No entanto, todos eles devem...
Eu encontrei um problema na prova de redução de assunto de Barendregt (Thm 4.2.5 do cálculo Lambda com tipos ). A última etapa da prova (página 60) diz: "e, portanto, pelo lema 4.1.19 (1), . "Γ,x:ρ⊢P:σ′Γ,x:ρ⊢P:σ′\quad\Gamma,x:\rho\vdash P:\sigma' No entanto, de acordo com o Lema 4.1.19 (1) ele...
Dado um termo t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))na teoria de tipos de Martin-Lof, qual é o valor de w(t(0)), onde westá o operador que extrai a testemunha de um termo de tipo
Lógicas condicionais são lógicas que aumentam a implicação lógica tradicional com operadores modais correspondentes a outras noções de condição (por exemplo, a condicional causal indica " A causa" B ", ou condicionamento probabilístico" A | B ", que lê" A dado B ").A□→BA◻→BA\; \square\!\!\!\!\to...
Alguns anos atrás, encontrei a seguinte regra de esquerda para a igualdade no cálculo sequencial: s ≐ t ⇝ θθ ( Γ ) ⊢ θ ( C)Γ , s ≐ t ⊢ Cs≐t⇝θθ(Γ)⊢θ(C)Γ,s≐t⊢C \frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t \vdash C} Aqui, s ≐ t ⇝ θs≐t⇝θs \doteq t...
Tenho uma pergunta ingênua: existe uma máquina de Turing cujo término é verdadeiro, mas não pode ser provado por nenhuma teoria natural, consistente e finamente axiomatizável? Peço uma mera prova de existência e não um exemplo específico. Isso pode ter alguma conexão com a análise ordinal . De...
No artigo clássico PLDI'98 de Necula, "O design e implementação de um compilador de certificação", o verificador de alto nível usa: VCGen para gerar condições de verificação (predicados de segurança) Provador do teorema da lógica de primeira ordem para provar as condições Verificador de prova LF...
Estou procurando trabalho em sistemas semelhantes às sequências de ordem superior de K. Dosen ("Sequent Systems for Modal Logic", JSL 50 ). O único trabalho que conheço é o trabalho recente de Iemhoff e Metcalfe ("Teoria da prova de regras admissíveis", Annals of Pure and Applic Logic 159 (1-2),...
Eu estive olhando para uma lógica modal com o axioma ( ◊ Um ∧ ◊ B ) → ◊ ( ( A ∧ ◊ B ) ∨ ( A ∧ B ) ∨ ( Um ∧ ◊ B ) )(◊UMA∧◊B)→◊((UMA∧◊B)∨(UMA∧B)∨(UMA∧◊B)) (\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B)) Grosso modo, isso diz que a...
Alguém poderia dar uma explicação intuitiva ( não intucionista) da correspondência da introdução à esquerda e eliminação da implicação no Cálculo Sequencial (SC) e Dedução Natural (ND), respectivamente? Eu sei que eles deveriam pela simetria de SC, mas não vejo como eles se correspondem. De maneira...