Contact Us!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place. Commercial Alternative to JupyterHub.

| Download

This notebook is a theorem prover for an extended syllogistic logic which allows one to make assertions about comparative cardinalities of finite sets. The logic is complete and efficiently decidable. If an assertion follows from a set of assumptions, this notebook displays the proof. If it doesn't follow, it outputs a counter-model.

Views: 114
License: GPL3
Image: ubuntu2004
Tweet
Share
Share
Kernel: Python 3 (system-wide)

Inference involving the sizes of sets

by Lawrence S. Moss

This notebook has an implementation of syllogistic logic plus cardinality comparison information. One can enter premises and a possible conclusion, and the program will either return a proof or a counterexample. The logic has 23 syllogistic rules plus ex falso quodlibet. It has no boolean connectives. It is sound and complete for interpretations in finite sets. The proof system comes from my 2016 paper "Syllogistic Logic with Cardinality Comparisons".

Enter the cell below by clicking on it and then typing shift-return.
load("sizesLM.py")

ccc
--------------------------------------------------------------------------- NameError Traceback (most recent call last) /tmp/ipykernel_516/1391208896.py in <cell line: 1>() ----> 1 ccc NameError: name 'ccc' is not defined
The rest of this notebook is a set of examples. You may copy or modify them. You also can find further things to do in the cell above. These are the only things going on in this notebook.
follows(['All a are b', 'Some a are a','All b are c'], 'All c are b')
--------------------------------------------------------------------------- NameError Traceback (most recent call last) /tmp/ipykernel_516/1974504622.py in <cell line: 1>() ----> 1 follows(['All a are b', 'Some a are a','All b are c'], 'All c are b') NameError: name 'follows' is not defined 
garrulous()
--------------------------------------------------------------------------- NameError Traceback (most recent call last) /tmp/ipykernel_516/3031566759.py in <cell line: 1>() ----> 1 garrulous() NameError: name 'garrulous' is not defined 
follows(['There are more x than y', 'There are more y than z'], 'There are more x than z')

The conclusion follows from the assumptions.

Here is a formal proof in our system:

1 There are more x than y Assumption 2 At least as many x as y More-Card 1 3 There are more y than z Assumption 4 There are more x than z More-Right 2 3 
rules()

Here is the full set of proof rules of the logic:

------------ axiom All x are x All x are y ------------------- antitone All non-y are non-x All x are non-x ---------------- zero All x are y All non-x are x ---------------- one All y are x All y are x ---------------------------------- subset card There are at least as many x as y There are at least as many x as y ------------------------------------------ card anti There are at least as many non-y as non-x All x are y There are at least as many x as y ----------------------------------- card mix All y are x There are at least as many x as non-x There are at least as many y as non-y --------------------------------------- half There are at least as many x as non-y There are at least as many x as non-x There are at least as many y as non-y Some non-x are non-y --------------------------------------- maj Some x are y All x are y All y are z ------------- Barbara All x are z There are at least as many x as y There are at least as many y as z ---------------------------------- card trans There are at least as many x as z Some x are y ------------- conversion Some y are x Some x are y ------------- Some Some x are x All x are y Some x are z ------------- Darii Some y are z Some y are y There are at least as many x as y ---------------------------------- card-some Some x are x There are more x than y ----------------------- more-some Some x are non-y There are more x than y ---------------------------------- more-card There are at least as many x as y There are more x than y There are at least as many y as z --------------------------------------- more left There are more x than z Some x are non-y All y are x -------------------------------------- more There are more x than y There are more x than y -------------------------------- more anti There are more non-y than non-x Some x are non-y --------------------------------------- strict half There are more y than non-x Some x are x There are at least as many y as non-y -------------------------------------- integer Some y are y There are at least as many x as non-x There are more y than non-y --------------------------------------- more right There are more x than z

The system does not have Reductio ad Absurdum,

since we only need Ex Falso Quodlibet:

Some x are y

No x are y

-------------- X

S

There are more x than y

There are at least as many y as x

------------------------------------ X

S

Here S is any sentence.

Notice that the (Maj) rule has three premises.

The system is complete: all valid consequences can be proved in it.

In fact, the X rule is only needed at the end of derivations.

follows(['Some x are x','No y are z', 'There are more z than y', 'All x are y'], 'There are more x than y')

The conclusion does not follow from the assumptions.

Here is a counter-model.

We take the universe of the model to be {0, 1, 2}.

follows(['There are more x than y','There are more y than z'], 'There are more x than z')

The conclusion follows from the assumptions.

Here is a formal proof in our system:

1 There are more x than y Assumption 2 At least as many x as y More-Card 1 3 There are more y than z Assumption 4 There are more x than z More-Right 2 3 
follows(['There are more x than z','There are more y than z'], 'There are more x than y')

The conclusion does not follow from the assumptions.

Here is a counter-model.

We take the universe of the model to be {0, 1}.

follows(['There are more x than z','There are more non-y than z','All y are x'], 'There are more x than y')

The conclusion does not follow from the assumptions.

Here is a counter-model.

We take the universe of the model to be {0, 1}.

follows(['There are more x than z','There are more z than a'], 'There are more x than y')

The conclusion does not follow from the assumptions.

Here is a counter-model.

We take the universe of the model to be {0, 1, 2, 3, 4}.

follows(['There are more x than z',
         'There are more z than a',
         'There are more a than b',
         'There are more b than c',
         'There are more y than x',
         'All y are x'],
        'There are more x than y')
The assumptions are inconsistent due to cardinality problems. So the conclusion follows from a contradiction: 1 There are more y than x Assumption 2 All y are x Assumption 3 At least as many x as y Subset Card 2 4 There are more x than y X 1 3 
rules()

Here is the full set of proof rules of the logic:

------------ axiom All x are x All x are y ------------------- antitone All non-y are non-x All x are non-x ---------------- zero All x are y All non-x are x ---------------- one All y are x All y are x ---------------------------------- subset card There are at least as many x as y There are at least as many x as y ------------------------------------------ card anti There are at least as many non-y as non-x All x are y There are at least as many x as y ----------------------------------- card mix All y are x There are at least as many x as non-x There are at least as many y as non-y --------------------------------------- half There are at least as many x as non-y There are at least as many x as non-x There are at least as many y as non-y Some non-x are non-y --------------------------------------- maj Some x are y All x are y All y are z ------------- Barbara All x are z There are at least as many x as y There are at least as many y as z ---------------------------------- card trans There are at least as many x as z Some x are y ------------- conversion Some y are x Some x are y ------------- Some Some x are x All x are y Some x are z ------------- Darii Some y are z Some y are y There are at least as many x as y ---------------------------------- card-some Some x are x There are more x than y ----------------------- more-some Some x are non-y There are more x than y ---------------------------------- more-card There are at least as many x as y There are more x than y There are at least as many y as z --------------------------------------- more left There are more x than z Some x are non-y All y are x -------------------------------------- more There are more x than y There are more x than y -------------------------------- more anti There are more non-y than non-x Some x are non-y --------------------------------------- strict half There are more y than non-x Some x are x There are at least as many y as non-y -------------------------------------- integer Some y are y There are at least as many x as non-x There are more y than non-y --------------------------------------- more right There are more x than z

The system does not have Reductio ad Absurdum,

since we only need Ex Falso Quodlibet:

Some x are y

No x are y

-------------- X

S

There are more x than y

There are at least as many y as x

------------------------------------ X

S

Here S is any sentence.

Notice that the (Maj) rule has three premises.

The system is complete: all valid consequences can be proved in it.

In fact, the X rule is only needed at the end of derivations.

follows(['Some x are z', 'There are more y than x', 'There are more x than z', 'There are at least as many x as h', 'There are more x than d', 'Some y are d', 'There are at least as many x as b', 'All x are e', 'All x are f', 'Some x are c', 'There are more a than b',  'There are more y than b'
  ],
        'There are more x than x')

The conclusion does not follow from the assumptions.

Here is a counter-model.

We take the universe of the model to be {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}.

follows(['All x are z', 'All w are y', 'All w are v', 'All k are w', 'All x are k', 'All k are non-v', 
        'Some y are x'], 'All x are y')
The assumptions are inconsistent due to cardinality problems. So the conclusion follows from a contradiction: 1 All y are y Axiom 2 No k are v Assumption 3 All k are w Assumption 4 All w are v Assumption 5 All k are v Barbara 3 4 6 All non-v are non-k Antitone 5 7 No k are k Barbara 2 6 8 No k are y Zero 7 9 All x are k Assumption 10 Some y are x Assumption 11 Some y are k Darii 9 10 12 Some y are non-y Darii 8 11 13 There are more y than y More 1 12 14 All y are y Axiom 15 At least as many y as y Subset Card 14 16 All x are y X 13 15 
follows(['All x are y', 'All z are w','All y are z'], 'All y are x')

The conclusion does not follow from the assumptions.

Here is a counter-model.

We take the universe of the model to be {0, 1}.

follows(['No c are a','All b are c','Some c are c', 'Some b are d', 'Some a are non-d'],'Some non-c are d')

The conclusion does not follow from the assumptions.

Here is a counter-model.

We take the universe of the model to be {0, 1, 2}.

follows(['All a are non-b', 'All non-b are c'], 'All non-c are non-a')

The conclusion follows from the assumptions.

Here is a formal proof in our system:

1 No a are b Assumption 2 All non-b are c Assumption 3 All a are c Barbara 1 2 4 All non-c are non-a Antitone 3 
follows(['There are more a than b','There are more b than c'],'There are more a than c')

The conclusion follows from the assumptions.

Here is a formal proof in our system:

1 There are more a than b Assumption 2 At least as many a as b More-Card 1 3 There are more b than c Assumption 4 There are more a than c More-Right 2 3 
rules()
--------------------------------------------------------------------------- NameError Traceback (most recent call last) <ipython-input-1-dd6d0f21abf7> in <module>() ----> 1 rules() NameError: name 'rules' is not defined 




import matplotlib_venn
from matplotlib_venn import venn3
--------------------------------------------------------------------------- ModuleNotFoundError Traceback (most recent call last) <ipython-input-7-2159f4810029> in <module>() ----> 1 import matplotlib_venn 2 from matplotlib_venn import venn3 ModuleNotFoundError: No module named 'matplotlib_venn' 
pre_process("All non-x are y")
['All', ('x', neg), ('y', pos)]