|
Descripción
|
|
|---|---|
| The practice of first-order logic is replete with meta-level concepts. Most notably there are meta-variables ranging over formulae, variables, and terms, and properties of syntax such as alpha-equivalence, capture-avoiding substitution and assumptions about freshness of variables with respect to metavariables. We present one-and-a-halfth-order logic, in which these concepts are made explicit. We exhibit both sequent and algebraic specifications of one-and-a-halfth-order logic derivability, show them equivalent, show that the derivations satisfy cut-elimination, and prove correctness of an interpretation of first-order logic within it. We discuss the technicalities in a wider context as a case-study for nominal algebra, as a logic in its own right, as an algebraisation of logic, as an example of how other systems might be treated, and also as a theoretical foundation for future implementation. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
JOURNAL OF LOGIC AND COMPUTATION |
|
ISSN
|
0955-792X |
|
Factor de impacto JCR
|
0,821 |
|
Información de impacto
|
|
|
Volumen
|
18 |
|
DOI
|
|
|
Número de revista
|
4 |
|
Desde la página
|
521 |
|
Hasta la página
|
562 |
|
Mes
|
NOVIEMBRE |
|
Ranking
|
|