Representing propositions in MeTTa (existential quantifier?)

[JungeWerther]

Let's say we have a statement "Bob has blue hair". We could represent it as a unary predicate like

(Predicate Object)
; or
(hasBlueHair Bob)

In case of a binary predicate like "Robin loves James", we can write

(Predicate Subject Object)
; or
(loves Robin James)

Universal quantification is most intuitively represented by an 'if' statement (functions are not appropriate, as discussed)
For example "all swans are black" could be represented as

(if (premise) (conclusion) ())
; or
(if (isSwan $x) (isBlack $x) ())

How would you represent the existential quantifier though? Obviously a predicate like (Exists $x) won't work. My initial thought is that it should be in a way 'dual' to the universal quantifier in the sense that A: all swans are black is equivalent to B: there does not exist a swan which is not black

So "there exists a black swan" could be "not all swans are not black"

(not (if (isSwan $x) (not (isBlack $x)) ()))

This is not equivalent to a direct assertion though, and you have to accept law of excluded middle.

As far as I'm aware you should be able to express quantified statements using dependent types in intuitionistic logic but I'm not sure how you would go about this in MeTTa.

What are your thoughts?

[JungeWerther]

Also, about the concept of negation.

let a: A represent a proof of some proposition A.

the analogue of not A would be A => _|_ constructively, where the logical contradiction corresponds to the uninhabited/empty type.

is this the same as
(: notA (=> A empty)) ?

[JungeWerther]

Okay here's what I learned:

An existential statement (exists x: X) . A
can be formalized as a pair (a, p) with a: X and p: A[a\x] (existential quantifier introduction).

So (exists x: Swan). isBlack x can be shown by a: Swan and isBlack a.

Crucially propositions like "all swans are black" are types and not 'normal' atoms so

(: $unaryPredicate (=> Object Bool))
(: $binaryPredicate (=> Subject Object Bool))

and so on.

Quantifiers should sit at the level of functions transforming proofs into proofs, not at the level of proofs.

I'm thinking

(: existsBlackSwan (=> (Swan, (=> Swan Bool)) Bool)

then, an observation

(: blackSwan Swan)
(: isBlack (=> Swan Bool))

(blackSwan, isBlack)

would suffice to prove

!(existsBlackSwan (blackSwan, isBlack))
> [true]

@Necr0x0Der
@vsbogd

is this similar to what you had in mind?

[ngeiswei]

What I've been using so far is, like you suggested, to use a dependent sum for existential quantification and a dependent product for universal quantification.

An example of dependent sum in MeTTa can be found here. As for dependent product, you can merely use the arrow type -> (I can dig up an example if you want me to).

[vsbogd]

Representation depends on how one would like to interpret the quantifiers. Here is an example of building existential and universal quantifiers as programs which returns unit when proposition is true and empty results otherwise.

(: whiteSwan1 Swan)
(: whiteSwan2 Swan)
(: blackSwan Swan)

(isWhite whiteSwan1)
(isWhite whiteSwan2)
(isBlack blackSwan)

(: negate (-> Atom (->)))
(= (negate $expr) (
  (case $expr (
    (() Empty)
    (Empty ())
  ))))

(= (evaluate $space $predicate)
  (trace! (quote (evaluate $space $predicate))
  (case $predicate (
    ((UQ $pattern $condition) (if (== (collapse (unify $space $pattern (negate (evaluate $space $condition)) ())) ()) () Empty))
    ((EQ $pattern $condition) (if (not (== (collapse (unify $space $pattern (evaluate $space $condition) Empty)) ())) () Empty))
    ($_ (match $space $predicate ()))
  ))))

!(evaluate &self (isWhite whiteSwan1))
!(evaluate &self (UQ (: $x Swan) (isWhite $x)))
!(evaluate &self (EQ (: $x Swan) (isBlack $x)))
!(evaluate &self (EQ (: $x Swan) (isWhite $x)))

One can also represent propositions as types or have predicates as a functions which return a boolean value.

[JungeWerther]

Hi @ngeiswei , I wanted to use your example of the dependent sum for reference but seems like the link is broken now, could you repost it?

Also, I've opened a reference thread here that I will be passing to annotators for the dataset - feel free to take a look or make suggestions if a specific representation synergizes with your use-case!

[Necr0x0Der]

In dependent types, one can treat existence in terms of the corresponding type to be not empty. In my understanding, it may look like this:

(: Swan (-> Entity Type)) ; Swan as "is-a" property of Entity
(: Crow (-> Entity Type)) ; Crow as "is-a" property of Entity
(: entity-001 Entity) ; some entity
(: entity-002 Entity) ; another entity
(: swan-001 (Swan entity-001)) ; the fact that entity-001 is a Swan
(: crow-001 (Crow entity-002)) ; the fact that entity-002 is a Crow
(: Black (-> Entity Type)) ; Black as a property
(: black-001 (Black entity-001)) ; the fact that entity-001 is Black
(: black-crows (-> (Crow $t) (Black $t))) ; the rule that all Crows are Black
; We may want to add something like:
; (: T Type)
; (= (black-crows $x) T)
; in MeTTa, there is no difference between a function and a type constructor,
; so black-crows is already a "proof"
; if we ignore the following as constructors,
(: black-swan-exists (-> ((Black $x) (Swan $x)) Type))
(: black-crow-exists (-> ((Black $x) (Crow $x)) Type))
; then we can consider the following as proofs
!(get-type (black-swan-exists (black-001 swan-001)))
!(get-type (black-crow-exists ((black-crows crow-001) crow-001)))

I don't like this representation too much, and MeTTa has some differences from Idris. Also, dependent types only allow to check the proof, so they don't seem to be enough. Automatic search for proofs will require searching for facts for corresponding statements. Thus, in fully constructive settings, you'll have to do something like:

!(match &self (, (: $c1 (Black $e1)) (: $c2 (Swan $e1))) (Proven by $e1))

And you don't need types for this. Your inference engine should search for proofs in any case.
It is not necessary to have proofs of existence as facts. Your engine can support general statements that something exists. But in this case, you'll need to have Exists as a dedicated symbol processed by your system.
But you can also consider existence, if you can get True for a variable argument, e.g.

(= (ift True $r) $r)
(= (ift $1 $2) Empty)

(= (swan entity-001) True)
(= (swan $_) Empty)

(= (crow entity-002) True)
(= (crow $_) Empty)

(= (black $x)
   (ift (crow $x) True))
(= (black entity-001)
   True)
(= (black $_) Empty)
(= (black-P-exists? $p)
   (ift (and ($p $x) (black $x)) True))
!(black-P-exists? swan)
!(black-P-exists? crow)
!(black-P-exists? clown)

It looks similar to Prolog. When you have free variables at right hand side, they act as they are under existence quantifier.
So, basically, there are different ways of handling existence. But as @vsbogd said, everything depends on how your inference engine works.

[Necr0x0Der]

The above might be not precise, when there are multiple proofs of existence (see the bottom of the comment here #40 (comment) ). Depending on the inference engine and purpose, collapse can be needed.