CODEWITHSUNDEEP
first-order-logiclean
user2222943
user2222943

Reputation: 15

How can I convert logical clause to LEAN?

I have a logical clause like this:

exists l.(language(l) & exists n.(name(n) & :op1(n,"English") & :name(l,n)))

which corresponds to the expression: "language is English"

The clause consists of the variables (l,n), predicates (language, name, op1) and constants ("English"). Each variable is assigned to its corresponding class first (l is assigned to "language" and n is assigned to "name") then the instance of a class is used for further inference (:op1 is a predicate assigning the constant "English" to the instance of the class "language". Or it can be considered as a property of a class "language").

Is there a way to convert this into LEAN code?

Upvotes: 0

Views: 134

Answers (1)

Kyle Miller
Kyle Miller

Reputation: 346

There are many ways you might map this into Lean, and it can depend greatly on what you're wanting to model exactly. In any case, here's one possibility.

Lean uses type theory, and one difference between type theory and first-order logic is that quantification is always bounded by a type, rather than there being a universal domain of discourse. Maybe the most idiomatic way to write this is as

namespace lang_ex

inductive language
| english

def name : language → string
| language.english := "English"

end lang_ex

This defines a new type called language that has one inhabitant called language.english, and it defines a function name that takes something with type language and yields a string (standing in for your name class). The rule for the function is that its value when given language.english is "English".

What these directives do, more or less, is define the following axioms:

namespace lang_ex

constant language : Type
constant language.english : language
constant name : language → string
axiom name_english : name language.english = "English"

end lang_ex

(There's no difference between constant and axiom -- they both introduce things axiomatically.) In Lean, function application syntax is by juxtaposition, so name language.english rather than name(language.english).

Here's an unidiomatic way to write it, following your clause as closely as possible:

namespace lang_ex

constant univ : Type
constant is_language : univ → Prop
constant is_name : univ → Prop
constant op1 : univ → string → Prop
constant name : univ → univ → Prop

axiom clause :
  ∃ (l : univ), is_language l ∧
    ∃ (n : univ), is_name n ∧ op1 n "English" ∧ name l n

end lang_ex

Upvotes: 3

Related Questions