Heimseite

Seitenübersicht

An/abmeldung

Warenkorb

Anschlagbrett

Herunterladen

(c) 2008-2019 XLOG Technologies GmbH

Author: Jan Burse, XLOG Technologies GmbH

Date: 14. February 2010

Version: 0.2

Participants: None

Jan Burse, XLOG Technologies
GmbH, 10. February 2010, 0.1:

- Initial Version.

Jan Burse, XLOG Technologies
GmbH, 14. February 2010, 0.2:

- Some fixes, such as the non-empty domain rule

Our recent logic investigation made use of the formula as type notion of construction while obtaining results for minimal logic and type theory. There is a close similarity between the additional formation rules in type theory and the deduction rules in minimal logic. We give an overview of the involved natural deduction style inference rules.

We close this document with a short summarization of the results that can be obtained for the given calculi. We will also highlight what might be still ahead on the road for us.

We first exhibit the minimal logic framework. A framework basically consists of some axiom schema and inference rule schemas. Some of the axioms and inference rules are marked as being subject to instantiate for various concrete calculi. The minimal logic is not a pure Hilbert style logic, since the (Right →) discharges some premise.

The inference rules are based
on sequents
of the following form. The x_{1}, …, x_{n} are proof
variables
and the t is a proof term:

A_{1} : x_{1},
…, A_{n} : x_{n} |- A : t

These proof objects are part of
the formula
as type notion of construction. A proof term is basically able to
denote a
proof. Whereas A_{1}, .., A_{n} and A can only carry
the
information of the premises and the conclusion.

Table
1: Minimal Logic
Framework

Γ |- A : t Δ |- A → B : s

---------------- (Id) -------------------------------- (MP)

A : x |- A : x Γ, Δ |- B : (s t)

Γ, [A : x] |- B : t Γ |- A : t, u ∉ G

---------------------- (Right →) ------------------- (Right ∀)

Γ |- A → B : lx.t Γ |- ∀uA : λu.t

Γ |- ∀uA : t

-------------------- (Inst) ----------- (Axiom)

Γ |- A[u/r] : (t r) |- A : c

The mark schema is (Axiom). For
a
particular calculus we assume that some set of axioms is given. The
formula A
that is introduced by the axiom has an associated constant c. This
constant is
the proof object for the axiom.

The unmarked schemas make use
of
implication (→)
and forall (∀).
Additional connectives and
quantifiers can be introduced via
mention inside new axioms. Negation is not a primitive connective, but
a short
hand as follows ¬
A = A → ⊥.

Table 2: Fragment
and Calculi Axioms

------------------------ ----------------------------------

|- A → (B → A · B) : f

--------------------- -----------------------------------

|- ∀u(A → ∃uA) : e

---------------------- ----------------- ----------------------------

|- ¬ ¬ A → A : n

The axioms f_{1} and f_{2}
allow the definition of a fusion connective. The axioms e_{1}
and e_{2}
allow the definition of an existential type quantifier. Adding the
axiom n_{1}
results in classical logic, adding the axiom n_{2} results in
intuitionist logic and finally the axiom n_{3} gives a
para-consistent
logic. It can be established that n_{2} + n_{3} = n_{1}:

Picture
1: Relationships
between the
Calculi

We already allow head variables and lambda expressions in proof objects. If we allow similar expressions in formulas we might quickly run into problems. A type theory allows restricting the formation of formulas. Whereby a deductive system is based on judgements of the following form:

type : term

Our type theory will make use of judgements of the following forms:

kind : type sort : kind

The former judgement is used to form families of types by relating them to kinds. The later judgement allows the formation of families of kinds. There will be new axiom schemas and inference rule schemas for kinds and sorts. We only use the arrow to form kinds. Thus if a and b are kinds, then a → b is also a kind.

We will also need to enhance the axioms and schemas known from minimal logic, in that we link them to some kind judgements. The basic kind “o” will play a special role. It is use to denote the family of types that make up propositions. The propositional connective of implication → has the kind o → (o → o), i.e. sending two propositions to a new proposition.

Propositional quantifiers will now be index by a kind a. Thus a quantifier ∀a will have the kind (a → o) → o, i.e. sending an abstraction over a proposition to a new proposition. Practically all axioms and inference rules of minimal logic needed to be modified, except for the modus ponens which is unchanged:

In typed minimal logic a derivation is not only based on propositional premises, the context might also contain assumption about kinds and sorts. An assumption about the kind of a variable is needed in the forall right introduction rule (Right ∀sa). The axiom schema (Non-Empty) states that the kinds are non-empty and is necessary to match the untyped minimal logic with the typed minimal logic:

Table
3: Typed Minimal
Logic Framework

Γ |- o : A Γ |- A : t Δ |- A → B : s

---------------- (Id) ---------------------------------- (MP)

Γ, A : x |- A : x Γ, Δ |- B : (s t)

Γ, [A : x] |- B : t Δ |- o : A Γ, [α : u] |- A : t Δ |- σ : α, u ∉ G

---------------------------- (Right →) ----------------------------- (Right ∀σα)

Γ, Δ |- A → B : lx.t Γ, Δ |- ∀

Γ |- ∀

------------------------------- (Inst

Γ, Δ |- A[u/r] : (t r) Γ |- A : c

|- o : ∃

----------------------- (Non-Empty)

|- ∃

The axioms and inference rules
for kinds and
sorts will regulate the available kinds and types based on sorts. The
marked
axioms and inference rules are (Idk), (lstr),
(∀s),
(∃s),
(Axiomk) and
(Axioms).
They regulate what variables, lambda abstractions,
forall
formulas, existential type formulas, constants and type constructors
can be
formed. The inference rule (MP k) and (MPs) are
unmarked. Separate rules for the quantifier formation are needed, since
a fragment
might allow less lambda abstraction than needed for the quantifier
formation:

Table
4: Type
Formation Framework

Γ |- σ : α Γ |- α : g Δ |- α → β : f

---------------- (Idσ) ---------------------------- (MPk)

Γ, α : u |- α : u Γ, Δ |- β : (f g)

Γ, [α : u] |- β

------------------------------- (λστρ) -------------- (Axiomk)

Γ, Δ |- (α → β)

Γ, [α : u] |- o : A Δ |- σ : α Γ, [α : u] |- o : A Δ |- σ : α

----------------------------- (∀σ) ------------------------------- (∃σ)

Γ, Δ |- o : ∀

Γ |- σ : β Δ |- σ → τ : α

------------------------------ (MPσ) --------- (Axioms)

Γ, Δ |- τ : (α β) |- σ : k

We will only consider fragments that conceptualize predicates and domain objects. For this purpose we will introduce the following basic kind “i”. This kind indicates individuals among the domain objects. Further the sort * will indicate predicates and the sort □ will indicate domain objects. Common among these fragments are the following formation axioms and inference rules:

Table
5:
Common
Kind Declarations

-------- (Individuals among Domain) -------- (Propositions are Predicates)

|- □ : i |- * : o

------------------- (Implication) ------------------ (Fusion)

|- o → (o → o) : → |- o → (o → o) : ·

------- (Falsum)

|- o : ⊥

Γ |- □ : α Γ |- * : α

------------ (Domain Constants) ------------ (Predicate Constants)

Γ |- α : h Γ |- α : h

We first started using our type formation framework to distinguish between first order logic and typed combinatorial logic. First order logic is not higher order. On the other hand typed combinatorial logic is higher order in the area of domain objects. The domain can contain functorials and variables can range over this domain. Further lambda abstraction over the domain is allowed. But it is not higher order what concerns predicates. It is not possible to have predicate variables and thus to quantify over predicate variables.

Table
6:
First Order Logic vs. Typed Combinatorial Logic

First Order Logic | Typed
Combinatorial Logic |

--------- |- ∇ : i |
N/A |

------------------------- |- ∇ → (□ → □) : → |
------------------------- |- □ → (□ → □) : → |

------------------------- |- ∇ → (* → *) : → |
------------------------- |- □ → (* → *) : → |

Γ |- ∇
: α ------------------- (Id∇) Γ, α : x |- α : x |
Γ |- □ : α ------------------ (Id□) Γ, α : x |- α : x |

N/A |
Γ, [α :
u] |- β^{□} :
r Δ |- □ : α----------------------------- (λ□□□) Γ, Δ |- (α → β) ^{□} : λu.r |

Γ, α : x |- o :
B
Δ |- ∇ : α ------------------------------ (∀∇) Γ, Δ |- o : ∀ _{α}xB |
Γ, α : x |- o :
B
Δ |- □
: α -------------------------- (∀□) Γ, Δ |- o : ∀ _{α}xB |

Γ, α : x |- o :
B
Δ |- ∇ : α -------------------------------- (∃∇) Γ, Δ |- o : ∃ _{α}xB |
Γ, α : x |- o :
B
Δ |- □
: α ---------------------------- (∃□) Γ, Δ |- o : ∃ _{α}xB |

Although we can exclude some paradoxes with type theory, the resulting fragments and calculi do not exhibit their full potential. Namely we will not be able to easily derive predicate comprehension. The remedy is surprisingly simple. All we need is to allow a form of conversion for abstraction over predicates. The additional axioms and inference rules are:

Table
7: Predicate Quantifiers
and Predicate
Conversion

Γ |- * : α

------------------ (Id*)

Γ, α : x |- α : x

Γ, α : x |- o : B Δ |- * : α Γ, α : x |- o : B Δ |- * : α

------------------------------ (∀*) --------------------------- (∃*)

Γ, Δ |- o : ∀

Γ, [α : u] |- β

---------------------------- (λ□**)

Γ, Δ |- (α → β)

-------------------------------------- --------------------------------------

|- B[y/t]r

We can add these extensions either to first order logic or to typed combinatorial logic. When the predicate quantifiers are added to first order logic, we will arrive at what is called generalized second order logic. This is a weak form of second order logic. When the predicate quantifiers and the predicate conversion are added to typed combinatorial logic, we arrive at what is called propositional type theory. This is a weak form of elementary type theory.

Picture
2:
Relationships between the Fragments

For all the fragments, it can be seen that we can freely add the dimension of negation from the previous section. Each of the fragments is available in its minimal, intuitionist, para-consistent and classical version. As can be seen from the axioms, we do not assume any domain equality, but logical identity can be easily defined as A ↔ B := (A → B) · (B → A) since implication and fusion are available.

Many of the following results are based on the fact that we have restricted ourselves to what we have called propositional type theory. The predicate conversion axioms are not to be confused with what is usually known as b-conversion. Predicate conversion can only be applied to the head of an element inside a sequent, it cannot be applied anywhere inside a formula. Further it can only be applied to the sort *, and not any other sort.

All of the results we will consider are independent on the dimension of negation. For these results marked still work in progress it is not yet clear whether and how all the fragments show the result, but at least the result was already established for some fragment:

- Lifting: Any derivation can be specialized.

- Inversion: Derivations ending in implication, forall and fusion can be inverted.

- Absorption: Derivations ending in existential type can be absorbed.

- Cut-elimination: There are pre-analytic rules which can derive the same as the natural deduction rules.

- Substitutability: Logical
identities can be replaced.

- Interpolation Variables: There is an interpolant for a split sequent based on variable side condition.

- Interpolation
Constants: There is an interpolant for a split sequent
based on
constants side
condition. Still work in progress.

- Interpolation Polarity: There is an interpolant for a split sequent based on polarity side condition. Still work in progress.

- Conservative Domain: A first order logic problem gives no other result in typed combinatorial logic. Still work in progress.

- Conservative Predicates: A typed combinatorial logic problem gives no other result in propositional type theory. Still work in progress.

- Beth Property: Unique implicit definitions give rise to explicit definitions. Still work in progress.

- Predicate Extensionality: When predicates are extensionally identical then we can replace them. Still work in progress.

- Beth Theorem: Unique implicit definitions that exist are identical to some explicit definition. Still work in progress.

- Definition Consistency: Consistent theories extended by hierarchical explicit definitions are consistent. Still work in progress.

- Definition Elimination: Extensions by hierarchical explicit definitions can be eliminated. Still work in progress.

All the above topics are quite interesting for logic programming. But logic programs do not usually consist only of hierarchical definitions of propositional predicates. We also observe recursion and meta-programming. Further logic programs are usually approached model theoretically. Therefore we see the following fundamental issues, which we would like to cover as well in the future:

- Definite Definitions: Definitions based on monotone operators have their syntactical correspondence in positive predicate occurrences. Any consistency or elimination theorems possible?

- Modal Operators: So called meta-predicates that take goals as arguments can be viewed as modal operators. Any consistency or elimination theorems possible?

- Kind
Parameters: In our typed combinatorial logic, we would already
need an
inference
rule schema
to only define for example the K combinator. To avoid schemas we could
allow
the forall quantifier inside kind expressions.

- Sort Hierarchies: When we look at our sort definitions for first order logic, we see an overloading of the kind “i”. But instead of stating that individuals are among the domain, we could have also stated that arguments are among the domain, resulting in an inference rule schema not yet found in the framework.

- Henkin Models: What interests here are not so much term models, but rather generalized models where the types Ta→b are not set theoretical maps from Ta to Tb. This is needed when Cantors theorem fails for the higher order domains.

- Residuated Lattices: It would be useful to have a common ground to define models for all the negations we have. These models should suite the connectives and quantifiers. This would consist of a more algebraic approach than non-normal semantics.

- Reflective Systems: In minimal first order logic, when a formula A does not contain the falsum ⊥, then we can also not derive the falsum ⊥ from the formula. If we analyse this meta-level result, we see that the premise could be modelled as a refined kind judgement. Further the consequence could be modelled as an existential type over proof objects. A reflective system would allow the former and the later as propositions.

- Generalized Type Systems: We have already highlighted the similarity of the inference rules on each level. In a generalized type system we would only model common inference rules once plus some parameterization of the interplay of the levels. This gives a more systematic account of the different fragments, simplifies the comparison with existing systems and eases the definition of embeddings.

- Truth Predicates: Truth predicates such as call/1 are found in many systems. They are based on a replication of the propositions inside the domain. They thus consists a more practical but also less secure approach than modal operators and reflective systems. Nevertheless we might obtain some results for such predicates.

Brown, C.E. (2007): Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church’s Type Theory, Studies in Logic Volume 10, Logic and Cognitive Systems, College Publications 2007

Benzmüller, C. et al (2008): Reasoning in Simple Type Theory, Festschrift in Honour of Peter B. Andrews on His 70th Birthday, Studies in Logic Volume 17, Mathematical Logic and Foundations, College Publications 2008

Sorensen M.H. et al (2006): Lectures on the Curry-Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, Volume 149, Elsevier 2006

Shapiro, S. (1991): Foundations without Foundationalism, Reprint, Oxford University Press 2002

Barendregt, H. (1991): Introduction to Generalized Type Systems, Journal of Functional Programming 1 (2), Page 125-154, April 1991

Dragalin, A.G. (1979): Mathematical Intuitionism, Introduction to Proof Theory, Translations of Mathematical Monographs Volume 67, American Mathematical Society 1988

Prawitz, D. (1965): Natural Deduction, A Proof-Theoretical Study, Reprint, Dover Publications, Inc. 2006

Curry, H.B. (1963): Foundations of Mathematical Logic, Reprint, Dover Publications, Inc. 1977