Leibniz' Project

A website aiming at global formalization

Table of contents

Rocq index

Lean index

Philosophy

Ethics

Ethics: first steps

Ethics in a society

If every individual ethic is objective, no possible disapproval iff everyone has the same ethic

More restrictive individual ethics diminish the risk of conflicts

Altruism is not enough to avoid conflicts

Ethics restrict goal achieving

Ethics restrict conflict winning

Philosophy of science

Occam's razor

The scientific process

Physical theories

The many-worlds interpretation

Physics with free will

Social choice

Economics

The gains from trade

Taxation

A definition of capitalism and communism in terms of redistribution of wealth

Pure capitalism is the only redistribution which makes financially independent

Maximizing the average work incentive

Pure communism is the only redistribution which maximizes the social utility

Politics

A definition of corruption

add1_lt (lemma)

add_comm (lemma)

add_positive_increases (lemma)

add_positive_increases_nonneg (lemma)

add_sums (lemma)

add_translation (lemma)

addq0l (lemma)

addq0r (lemma)

addq_opp (lemma)

admits_omnipotent (definition)

AggregateTransaction (definition)

aggregation_preferences (definition)

agree_on (definition)

agree_on_implies_remove_indifference_equal (lemma)

agree_on_implies_remove_indifference_equal_profile (lemma)

agree_on_profile (definition)

altruist (definition)

always_follows_its_ethic (definition)

antecedent (definition)

antecedent_exists (lemma)

antecedent_not_exists (lemma)

Arrow (theorem)

assertion_1 (lemma)

assertion_2 (lemma)

assertion_3 (lemma)

assertion_4 (lemma)

associatedPreferenceSpace (definition)

assymmetric (definition)

at_least_as_productive (definition)

average_in_between (lemma)

average_nonneg (definition)

barter (definition)

barter_AggregateTransaction (definition)

barter_preserves_total_production (lemma)

barter_tr (definition)

bipartite_contest (definition)

bool_eq_equal (lemma)

bottom_choice (definition)

bound_nonneg (definition)

bound_nonneg_to_reals (lemma)

brought_insight (definition)

Capacity (definition)

capacity_is_finite (lemma)

comparative_advantage (definition)

compatible (definition)

completeness_nonneg (definition)

conflict (definition)

Constitution (definition)

corollary_2 (corollary)

corollary_3 (corollary)

countable (definition)

dead_end (definition)

deterministic_iff_no_indeterminism (lemma)

deterministic_many_worlds_interpretation (lemma)

deterministic_World (definition)

dictator (definition)

dictator_except (definition)

div_nonneg (definition)

dominant (definition)

dominant_strategies_profile (definition)

dominant_strategies_well_named (lemma)

dominant_strategy (definition)

efficient (definition)

eq_symmetric (lemma)

equal_nonneg_if_equal_reals (lemma)

equipotent (definition)

Ethic (definition)

ethic_restricts_conflict_winning (lemma)

ethic_restricts_goal_achieving (lemma)

ethic_restricts_goal_achieving_with_ethics (lemma)

ethic_strictly_restricts_goal_achieving (lemma)

ethic_subjective_to_dynamic (definition)

ethicless (definition)

ethicless_least_restrictive (lemma)

ethics_cant_help_goal_achieving (lemma)

Event (definition)

every_ethic_more_restrictive_than_itself (lemma)

everyone_always_follows_its_ethic_dynamic (definition)

everyone_always_same_ethic (definition)

everyone_follows_its_ethic (definition)

everyone_follows_its_ethic_dynamic (definition)

everyone_is_objective (definition)

everyone_same_ethic (definition)

exists_dominant_strategy (lemma)

exists_of_not_extremal (lemma)

exists_pivot (lemma)

exists_pivot_when_hater (lemma)

extend_nonneg_reals (definition)

extend_nonneg_reals_inv (lemma)

extend_nonneg_reals_prop (lemma)

extend_reals_nonneg (definition)

extend_reals_nonneg_inv (lemma)

extends_before (definition)

extends_until (definition)

extremal_lemma (lemma)

false_to_False (lemma)

finite_precision_possible_qty (definition)

finite_production (definition)

follows_its_ethic (definition)

follows_policy (definition)

follows_policy_before (definition)

fulfilled_goal (definition)

fulfills_goal (definition)

GameForm (definition)

generalized_whole_society (definition)

get_action (definition)

get_carrier (definition)

get_h1 (definition)

get_h2 (definition)

get_injection (definition)

get_preference_order (definition)

get_state (definition)

get_SubjectiveState (definition)

get_t1 (definition)

get_t2 (definition)

get_time (definition)

Gibbard (theorem)

GibbardSatterthwaite (corollary)

GoalProfile (definition)

gt_upper_bound_is_upper_bound (lemma)

gt_upper_bound_is_upper_bound_nonneg (lemma)

happened_before (definition)

happens_in (definition)

has_pivot (definition)

History (definition)

History_offset (definition)

History_restriction_Before (definition)

HistoryBefore (definition)

HistoryBefore_restriction (definition)

HistoryUntil (definition)

HistoryUntil_restriction (definition)

identity (definition)

ignore_actions (definition)

in_capacity (definition)

in_image (definition)

in_total_capacity (definition)

incompatible (definition)

independence_irrelevant_alternatives (definition)

Indeterminism (definition)

indeterministic_iff_any_indeterminism (lemma)

indifferent (definition)

indifferent_if_non_strict_both_ways (lemma)

indifferent_reflexive (lemma)

indifferent_symmetric (lemma)

indifferent_transitive (lemma)

individual_follows_policy (definition)

individual_fulfills_goal (definition)

individual_may_achieve (definition)

IndividualEthic (definition)

IndividualPolicy (definition)

IndividualRank (definition)

IndividualsPermutationsActingOnStates (definition)

inj_implies_antecedent_unique (lemma)

instance_indeterminism (definition)

irreflexive (definition)

is_capacity (definition)

is_deterministic (definition)

is_deterministic_except_for_free_will (definition)

is_lub_nonneg (definition)

is_lub_nonneg_to_reals (lemma)

is_lub_reals_to_nonneg (lemma)

is_pivotal (definition)

is_possible (definition)

is_upper_bound_nonneg (definition)

law_opportunity_cost (lemma)

le_0_nat_to_rat (lemma)

le_bool_equivalent (lemma)

le_preference_order (lemma)

le_PreferenceOrder (definition)

le_rat_reflexive (lemma)

le_rat_S (lemma)

le_rat_transitive (lemma)

le_ratM0 (lemma)

le_total (lemma)

le_transitive (lemma)

least_upper_bound (definition)

least_upper_bound_is_upper_bound (lemma)

least_upper_bound_is_upper_bound_nonneg (lemma)

least_upper_bound_le_if_all_lt (lemma)

least_upper_bound_le_if_all_lt_nonneg (lemma)

least_upper_bound_nonneg (definition)

least_upper_bound_possible_qty (definition)

least_upper_bound_possible_qty_is_upper_bound (lemma)

lt_0_nat_to_rat (lemma)

lt_bool_equivalent (lemma)

lt_bool_equivalent_not (lemma)

lt_rat0M (lemma)

lt_rat_0_1 (lemma)

lt_rat_irreflexive (lemma)

lt_ratM0 (lemma)

make_above (definition)

make_above_preference (definition)

make_above_preference_order (lemma)

make_above_profile (definition)

make_above_total (lemma)

make_above_transitive (lemma)

make_above_well_named (lemma)

make_very_bottom (definition)

make_very_bottom_preference (definition)

make_very_bottom_preference_order (lemma)

make_very_bottom_total (lemma)

make_very_bottom_transitive (lemma)

make_very_top (definition)

make_very_top_at (definition)

make_very_top_preference (definition)

make_very_top_preference_order (lemma)

make_very_top_total (lemma)

make_very_top_transitive (lemma)

make_very_top_well_named (lemma)

manipulable (definition)

many_worlds_extension (definition)

map_PreferenceOrder (definition)

map_relation (definition)

may_achieve (definition)

may_achieve_all (definition)

may_achieve_ethically (definition)

may_achieve_with_ethics (definition)

may_all_achieve_ethically (definition)

may_disapprove (definition)

may_never_disapprove (definition)

may_not_win_conflict (definition)

may_not_win_conflict_with_ethics (definition)

may_win_conflict (definition)

may_win_conflict_with_ethics (definition)

more_adequate_in_deterministic_environment (definition)

more_intelligent_in_deterministic_environment (definition)

more_powerful (definition)

more_precise (definition)

more_restrictive (definition)

more_restrictive_dynamic (definition)

more_restrictive_ethic_diminishes_conflicts (proposition)

more_restrictive_ethic_strictly_diminishes_conflicts (proposition)

mulq0l (lemma)

mulq0r (lemma)

mulq1l (lemma)

mulq1r (lemma)

mulq_addr (lemma)

mulq_inv (lemma)

mult_nonneg (definition)

nat_to_rat (definition)

nat_to_rat_0 (lemma)

nat_to_rat_inj (lemma)

no_conflict (definition)

no_dead_end_if_altruist (lemma)

no_dead_end_if_conflict (definition)

no_dead_end_if_everyone_follows_its_ethic (lemma)

no_dead_end_if_no_conflict (definition)

no_ethic_strictly_more_restrictive_than_itself (lemma)

no_one_does_anything_gives_no_production (lemma)

no_transaction (definition)

nobody_may_disapprove (definition)

nobody_may_ever_disapprove (definition)

non_strict (definition)

non_strict_stable_by_indifferent (lemma)

non_strict_stable_by_indifferent' (lemma)

non_strict_strict_transitive (lemma)

non_strict_transitive (lemma)

nonneg_involution (lemma)

nonneg_proj_real (lemma)

not_0_nat_to_rat (lemma)

not_bigger_than (definition)

not_bigger_than_transitive (definition)

not_extremal (lemma)

not_very_top_or_not_very_bottom (lemma)

objective (definition)

objective_ethics_may_never_disapprove_implies_same_ethic (proposition)

objective_ethics_no_disapproval_iff_same_ethic (corollary)

occam_preferred (definition)

omnipotent (definition)

opportunity_cost (definition)

opportunity_cost_nonnegative (lemma)

outcome_when_dominant_strategies (definition)

pairwise_determination (lemma)

permutation_Event (definition)

permutation_History (definition)

permutation_State (definition)

permutation_SubjectiveState (definition)

PermutationsActingOnFunctions (definition)

PhysicalTheory (definition)

pivot_implies_dictator (lemma)

pivot_implies_dictator_except (lemma)

plus_nonneg (definition)

Policy (definition)

possible_targeted_production (definition)

possible_targeted_production_0 (lemma)

preference_antisym_iff_total_order (lemma)

preference_order (definition)

preference_order_reflexive (lemma)

preference_order_stable_by_flip (lemma)

preference_order_stable_by_map (lemma)

PreferenceOrder (definition)

PreferenceSpace (structure)

preferred_when_dominant_strategies (definition)

preferred_when_dominant_strategies_strict_implies_nonstrict (lemma)

preserves_total_production (definition)

production_decreasable_at_will (definition)

Profile (definition)

profile_III (definition)

proj_individual_SubjectiveState (lemma)

proj_state_SubjectiveState (lemma)

Quantity (definition)

quotient_le_1 (lemma)

rat_inv_0_lt_compat (lemma)

rat_inv_neq_0_compat (lemma)

rat_le_0_opp (lemma)

rat_le_opp_0 (lemma)

rat_lt_0_opp (lemma)

rat_lt_opp_0 (lemma)

rat_mul_minus_distr_r (lemma)

rat_mul_nonnulls_is_nonnull (lemma)

rat_mult_div_swap (lemma)

rat_mult_inj_r (lemma)

rat_mult_lt_compat_r (lemma)

rat_opp_involutive (lemma)

rat_opp_mul (lemma)

rat_opp_plus_distr (lemma)

rat_plus_inj_l (lemma)

rat_plus_inj_r (lemma)

rat_plus_le_compat_l (lemma)

rat_plus_le_compat_r (lemma)

rat_plus_lt_compat_l (lemma)

rat_plus_lt_compat_r (lemma)

rat_plus_minus_l (lemma)

rat_plus_opp_r_uniq (lemma)

rationals_isMonoidLaw_axioms (definition)

rationals_Monoid_isComLaw_axioms (definition)

rationals_Monoid_Law (definition)

rationals_SemiGroup_com_law (definition)

rationals_SemiGroup_isCommutativeLaw_axioms (definition)

rationals_SemiGroup_isLaw_axioms (definition)

ratz_0 (lemma)

ratz_1 (lemma)

ratz_inj (lemma)

Rdiv_le_0_compat (lemma)

reals_HB_associative (definition)

reals_HB_commutative (definition)

reals_isMonoidLaw_axioms (definition)

reals_Monoid_isComLaw_axioms (definition)

reals_Monoid_Law (definition)

reals_SemiGroup_com_law (definition)

reals_SemiGroup_isCommutativeLaw_axioms (definition)

reals_SemiGroup_isLaw_axioms (definition)

remove_indifference (definition)

remove_indifference_down_to_littlest_subset (lemma)

remove_indifference_in_Z_out_Z (lemma)

remove_indifference_is_preference_order (corollary)

remove_indifference_is_total_order (lemma)

remove_indifference_PreferenceOrder (definition)

remove_indifference_PreferenceProfile (definition)

remove_indifference_profile (definition)

remove_indifference_profile_down_to_littlest_subset (lemma)

remove_indifference_strict_unchanged_on_Z (lemma)

remove_indifference_well_named (lemma)

repartition_before_Ricardo_barter (definition)

respects_unanimity (definition)

reverse (definition)

reverse_very_bottom (lemma)

Ricardo (theorem)

Ricardo_barter (definition)

Ricardo_barter_enough_i (lemma)

Ricardo_barter_enough_j (lemma)

Ricardo_ineq_i (lemma)

Ricardo_ineq_j (lemma)

Rle_implies_minus_nonneg (lemma)

Rminus_2_1 (lemma)

Rminus_le_reg_r (lemma)

S_nat_to_rat (lemma)

same_ethic_implies_may_not_disapprove (lemma)

same_order (definition)

same_order_characterization (lemma)

same_order_non_strict (lemma)

same_order_reflexive (lemma)

same_order_strict_case (lemma)

same_order_symmetric (lemma)

satisfies (definition)

satisfies_before (definition)

satisfies_until (definition)

ScientificTheory (definition)

second_equal_or_1st_unequal (definition)

second_equal_or_1st_unequal_preference_order (lemma)

single_bottom_others_indifferent (definition)

single_bottom_very_bottom (lemma)

single_min_all_others_indifferent_preference_profile (definition)

single_top_others_indifferent (definition)

single_top_very_top (lemma)

smaller_than (definition)

smaller_than_assymmetric (lemma)

smaller_than_irreflexive (lemma)

smaller_than_transitive (definition)

State_dynamic (definition)

state_dynamic (definition)

state_dynamic_to_subjective (definition)

straightforward (definition)

Strategizing (definition)

Strategy_VotingScheme (definition)

StrategyProfile (definition)

StrategyProfile_VotingScheme (definition)

strict (definition)

strict_asymmetric (lemma)

strict_implies_non_strict (lemma)

strict_implies_unequal (lemma)

strict_irreflexive (lemma)

strict_le_is_lt (lemma)

strict_non_strict_transitive (lemma)

strict_non_strict_transitive_preference (lemma)

strict_preference (definition)

strict_preference_implies_non_strict (lemma)

strict_preference_transitive (lemma)

strict_transitive (lemma)

strictly_more_intelligent_in_deterministic_environment (definition)

strictly_more_powerful (definition)

strictly_more_restrictive (definition)

strictly_more_restrictive_dynamic (definition)

strictly_preferred_when_dominant_strategies (definition)

strictly_preferred_when_dominant_strategies_respects_unanimity (corollary)

sub_n_n_0 (lemma)

SubjectiveState (structure)

subq_gt0 (lemma)

switch_strict_preference_is_preference (lemma)

switch_strictness (definition)

switch_strictness_involutive (lemma)

switch_strictness_preferred_when_dominant_strategies (lemma)

switch_strictness_preferred_when_dominant_strategies' (lemma)

targeted_capacity_is_finite (lemma)

third_alt (definition)

time_translation_symmetry (definition)

top_choice (definition)

total (definition)

total_is_reflexive (lemma)

total_order (definition)

total_order_is_antisymmetric_preference (lemma)

total_production (definition)

total_stable_by_flip (lemma)

TotalOrder (definition)

transitivity_stable_by_flip (lemma)

unanimous_altruism_not_enough_to_avoid_conflicts (proposition)

unanimous_very_bottom (lemma)

unanimous_very_bottom_choice (definition)

unanimous_very_extremal_choice (definition)

unanimous_very_top (lemma)

unanimous_very_top_choice (definition)

unanimously_prefers (definition)

unanimously_same_order (definition)

unanimously_same_order_symmetric (lemma)

unanimously_unproductive (definition)

unproductive (definition)

unproductive_in_capacity (lemma)

upper_bound_nonneg_reals (lemma)

valq_numq_denq (lemma)

very_bottom_choice (definition)

very_extremal_choice (definition)

very_top_choice (definition)

VotingScheme (definition)

who_can_do_more_can_do_less (lemma)

who_can_do_more_can_do_less_global (lemma)

with_constraints (definition)

without_dead_end (definition)

WorkProduct (definition)

zero_nonnegreal (definition)

accounts_at_equilibirum (definition)

average_work_incentive (definition)

average_work_incentive_as_integral (lemma)

average_work_incentive_le_1 (theorem)

average_work_incentive_neg_eq_1 (theorem)

average_work_incentive_neg_is (definition)

average_work_incentive_pos_is (definition)

average_work_incentive_pos_le_1 (theorem)

average_work_incentive_until_neg (definition)

average_work_incentive_until_pos (definition)

can_decide_unilaterally (definition)

capitalism_encourages_work (lemma)

capitalism_is_egalitarian (lemma)

capitalism_is_fair (lemma)

capitalism_is_strictly_fair (lemma)

capitalism_maximizes_average_work_incentive (lemma)

change_currency_Redistribution (definition)

communism_encourages_work (lemma)

communism_except_extremal_contributors (definition)

communism_except_extremal_contributors_at_equilibirum (lemma)

communism_except_extremal_contributors_maximizes_average_work_incentive (lemma)

communism_except_extremal_contributors_Redistribution (definition)

communism_is_egalitarian (lemma)

communism_is_fair (lemma)

communism_maximizes_social_utility (theorem)

communism_not_strictly_fair (lemma)

continuousOn_Ici_to_uIcc_v1 (theorem)

corruption_opportunity (definition)

corruption_prone (definition)

currency_change (definition)

currency_change_at_equilibrium (lemma)

currency_change_distribution (definition)

currency_change_distribution_inverse (definition)

currency_change_inverse (definition)

currency_change_redistribution (definition)

dead_end (definition)

decide_unilaterally (definition)

differentiableAt_Ici_to_uIcc (theorem)

differentiableAt_Ici_to_uIcc_all (theorem)

differentiableAt_Iic_to_uIcc (theorem)

differentiableAt_Iic_to_uIcc_all (theorem)

div_le_div_of_pos (theorem)

encourages_work (definition)

Ethic (definition)

ethicless (definition)

ethicless_least_restrictive (theorem)

every_ethic_more_restrictive_than_itself (theorem)

everyone_always_same_ethic (definition)

everyone_is_objective (definition)

everyone_same_ethic (definition)

get_carrier (definition)

get_SubjectiveState (definition)

global_average_work_incentive_is (definition)

greatest_contributor (definition)

identity (definition)

increases_with_money (definition)

indifferent (definition)

indifferent_refl (lemma)

individual_contribution_atBot_dominates_sum_other_retributions (definition)

IndividualEthic (definition)

IndividualsPermutationsActingOnStates (definition)

inhabited_implies_nonnull_card (lemma)

instantaneous_work_incentive (definition)

instantaneous_work_incentive_capitalism (lemma)

instantaneous_work_incentive_communism (lemma)

inverse_currency_change (lemma)

inverse_currency_change_distribution (lemma)

is_egalitarian (definition)

is_fair (definition)

is_strictly_fair (definition)

law_diminishing_marginal_utility (definition)

law_diminishing_marginal_utility_strict (definition)

least_contributor (definition)

lim_frac_deg_1_0_bot (lemma)

lim_frac_deg_1_0_top (lemma)

lim_inverse_bot (lemma)

lim_inverse_top (lemma)

lim_neg_bot (lemma)

lim_neg_top (lemma)

maximizes_average_work_incentive (definition)

may_disapprove (definition)

may_never_disapprove (definition)

MonetaryValue (definition)

more_restrictive (definition)

ne_least_greatest_contributor (lemma)

no_ethic_strictly_more_restrictive_than_itself (theorem)

nobody_may_disapprove (definition)

nobody_may_ever_disapprove (definition)

non_mutual_strict (lemma)

non_strict_strict_transitive (lemma)

non_strict_transitive (lemma)

objective (definition)

objective_ethics_may_never_disapprove_implies_same_ethic (theorem)

only_communism_maximizes_social_utility (theorem)

only_pure_capitalism_makes_independent (theorem)

permutation_State (definition)

permutation_SubjectiveState (definition)

PermutationsActingOnFunctions (definition)

preference_order (definition)

preference_order_reflexive (lemma)

PreferenceOrder (definition)

PreferenceSpace (structure)

prefers (definition)

prefers_or_indifferent (definition)

proj_individual_SubjectiveState (lemma)

proj_state_SubjectiveState (lemma)

pure_capitalism (definition)

pure_capitalism_costs_equally_divided (definition)

pure_capitalism_costs_equally_divided_0 (lemma)

pure_capitalism_costs_equally_divided_at_equilibirum (lemma)

pure_capitalism_costs_equally_divided_Redistribution (definition)

pure_capitalism_Redistribution (definition)

pure_communism (definition)

pure_communism_at_equilibirum (lemma)

pure_communism_Redistribution (definition)

Redistribution (definition)

replace (definition)

replace_changes (theorem)

replace_unchanges (theorem)

represented_by_continuous_utility (definition)

represented_by_utility (definition)

retribution_depends_only_on_own_contribution (definition)

retribution_depends_only_on_own_contribution_capitalism (lemma)

retribution_function (definition)

Rpos (definition)

same_ethic_implies_may_not_disapprove (lemma)

self_interest_can_prevail (definition)

self_interest_prevails (definition)

single_greatest_contributor (definition)

single_greatest_contributor_unique (lemma)

single_least_contributor (definition)

single_least_contributor_unique (lemma)

social_utility (definition)

strict_implies_unequal (lemma)

strict_non_strict_transitive_preference (lemma)

strict_preference_implies_non_strict (lemma)

strict_transitive (lemma)

strictly_more_restrictive (definition)

SubjectiveState (structure)

sum_other_retributions_positive_if_individual_contribution_big_enough (definition)

sum_rationals_mult_constant (lemma)

sum_rationals_perm (lemma)

sum_rationals_sub (lemma)

sum_reals_div_constant (lemma)

sum_reals_mult_constant (lemma)

sum_reals_perm (lemma)

sum_reals_sub (lemma)

sum_split_two (theorem)

total_value (definition)

uIcc_nonneg_subset_Ici (lemma)

uIcc_nonpos_subset_Iic (lemma)

union_of_singletons_finset (theorem)

upstanding (definition)

upstanding_choice (definition)

without_dead_end (definition)

work_incentive_between (definition)

work_incentive_capitalism_between (lemma)

work_incentive_communism_between (lemma)