EVEN, the parity of the universe
Lax945089.Even · concepts/Lax945089/Even.lean · lax-945089
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance is a bare finite set, a structure over the empty vocabulary. It is a yes-instance of EVEN when its number of elements is even; EVEN is the decision problem of the structures isomorphic to such an instance, that is, of the sets of even size.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Basic |
| 2 | import Mathlib.SetTheory.Cardinal.Finite |
| 3 | import Mathlib.Algebra.Group.Even |
| 4 | import Lax904597.Problems |
| 5 | import Lax485149.Problems |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: EVEN, the parity of the universe |
| 10 | type: definition |
| 11 | --- |
| 12 | An instance is a bare finite set, a structure over the empty vocabulary. It |
| 13 | is a yes-instance of EVEN when its number of elements is even; EVEN is the |
| 14 | decision problem of the structures isomorphic to such an instance, that is, |
| 15 | of the sets of even size. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax945089.Even |
| 19 | |
| 20 | open FirstOrder FirstOrder.Language |
| 21 | open Lax904597.Problems Lax485149.Problems |
| 22 | |
| 23 | /-- EVEN: does the universe have an even number of elements? -/ |
| 24 | def EVEN : DecisionProblem Language.empty := |
| 25 | DecisionProblem.ofPred fun A _ => Even (Nat.card A) |
| 26 | |
| 27 | end Lax945089.Even |
| 28 |
Builds on
Used by
Lax945089.EhrenfeuchtMethodologyLax945089.EvenInvarianceLax945089.EvenNotFirstOrderLax945089.FirstOrderBelowACZeroLax945089.FirstOrderBelowTransitiveClosureLax945089.GamesOnLinearOrdersLax945089.GamesOnSetsLax945089.NoDefinableOrderLax945089.OrderFreeInductionMissesPTIMELax945089.ParityInLogSpaceLax945089.PebbleInvarianceLax945089.ReductionsBelowLogSpace
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments