Luì

Loading…

Luì

Luì is an online software dedicated to mathematical proof. The software is useful for discussing certain dynamics related to the proof process as well as for handling the formal aspects of that process.

In the game Luì, Proponent and Opponent challenge each other on a statement.

P thinks the statement is true, while O thinks the statement is false.

The statement is written in the form ∀x (H₁, ..., H_n → C), to be read as:
if for x the hypotheses H₁, ..., H_n hold,

During the game, P and O discuss the statement.
The basic idea of their dialogue is this: to say that a statement of the form ∀x (H₁, ..., H_n → C) is false,

For example, if one wants to argue that the sentence \"all birds can fly\", which in the form just presented is ∀x (BIRD(x) → FLY(x)), is false, one must find a bird t that cannot fly.

In the game, the hypotheses H are indicated in orange, while the conclusion C in blue.

P wins if they can leave O with no possibility to rebut. O wins if the game lasts indefinitely.

Download a complete game guide by CLICKING HERE!

Propositional Logic First-Order Logic

In PROPOSITIONAL LOGIC, the quantifier ∀ does not appear, and the discussion revolves around simple statements with hypotheses and conclusion.
A letter (A, B, C, ...) indicates any s

The TARSKI game mode is not yet ready!

We recommend starting with the SHORTCUT mode because it is more convenient. The rules for both modes can be found inside the guide.

Shortcut Mode Standard Mode

Proponent vs Opponent Proponent vs

GIUSEPPE PEANO

Giuseppe Peano was born in 1858 in a hamlet of Cuneo. It is said that, as a boy, he had to walk many kilometers every day to go to school, as is still typical today in many parts of the world. He then continued his studies in Turin thanks to his matern

AUOQUAMEL

Abū Kāmil Shujāʿ ibn Aslam, also known as al-Ḥāsib al-Miṣrī (\"The Egyptian Calculator\") and in the West as Auoquamel, was an Egyptian mathematician who lived around the years 850-930, during the Islamic Golden Age. The Islamic Golden Age is a period

JEAN-LOUIS KRIVINE

Jean-Louis Krivine is a French scholar, born in 1939, who has worked in mathematical logic, set theory, and theoretical computer science. He was a student at the École Normale Supérieure in Paris and then taught for many years at the University “Paris

GAME IN ON THE FORMULA

to play: click on formula you believe is false.

Proponent Wins!

The Opponent has nothing left to retort.

The conclusion is not in , choose another formula!

The conclusion is not in nor it is false, choose another formula!

The formula is false, choose another one

The predicate is not handled by SHORTCUT mode: if you think the statement is true, try to prove it using the axioms of $\"Top\"$ !

The equality is false, it's correct that it is in $\"Bot\"$ !

The conclusion is not in $\"Bot\"$ and is not a false equality either: try different numbers or another formula!

The predicate is false, it's correct that it is in $\"Bot\"$ !

The conclusion is not in $\"Bot\"$ and is not false either: try different numbers or another formula!

The expression is incorrect, type another one

The game is over! The player is the winner!

The set $\"T\"$ contains what is true for both players.

The set O_⊤ contains what O affirms to be true.

The set P_⊤ contains what P affirms to be true.

The set $\"T\"$ contains what is false for both players.

Moves

No moves made yet

Privacy Policy Terms & Conditions Disclaimer

oiler® 2026