| Texto completo | |
| Autor(es): |
Agudelo-Agudelo, Juan C.
;
Carnielli, Walter
Número total de Autores: 2
|
| Tipo de documento: | Artigo Científico |
| Fonte: | BULLETIN OF SYMBOLIC LOGIC; v. N/A, p. 25-pg., 2025-03-03. |
| Resumo | |
A Constructive Logic of Evidence and Truth ( $\mathsf {LET_C}$ ) is introduced. This logic is both paraconsistent and paracomplete, providing connectives for consistency and determinedness that enable the independent recovery of explosiveness and the law of excluded middle for specific propositions. Dual connectives for inconsistency and undeterminedness are also defined in $\mathsf {LET_C}$ . Evidence is explicitly formalised by integrating lambda calculus terms into $\mathsf {LET_C}$ , resulting in the type system $\mathsf {LET_C<^>{\lambda }}$ . In this system, lambda calculus terms represent procedures for constructing evidence for compound formulas based on the evidence of their constituent parts. A realisability interpretation is provided for $\mathsf {LET_C}$ , establishing a strong connection between deductions in this system and recursive functions. (AU) | |
| Processo FAPESP: | 20/16353-3 - Racionalidade, Lógica e Probabilidade- RatioLog |
| Beneficiário: | Marcelo Esteban Coniglio |
| Modalidade de apoio: | Auxílio à Pesquisa - Temático |