ﻻ يوجد ملخص باللغة العربية
We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an intensional or effective view of respectively ill-and well-foundedness properties to an extensional or ideal view of these properties. After classifying and analysing the relations between different intensional definitions of ill-foundedness and well-foundedness, we introduce, for a domain $A$, a codomain $B$ and a filter $T$ on finite approximations of functions from $A$ to $B$, a generalised form GDC$_{A,B,T}$ of the axiom of dependent choice and dually a generalised bar induction principle GBI$_{A,B,T}$ such that: GDC$_{A,B,T}$ intuitionistically captures the strength of $bullet$ the general axiom of choice expressed as $forall aexists b R(a, b) Rightarrowexistsalphaforall alpha R(alpha,alpha(a))$ when $T$ is a filter that derives point-wise from a relation $R$ on $A times B$ without introducing further constraints, $bullet$ the Boolean Prime Filter Theorem / Ultrafilter Theorem if $B$ is the two-element set $mathbb{B}$ (for a constructive definition of prime filter), $bullet$ the axiom of dependent choice if $A = mathbb{N}$, $bullet$ Weak K{o}nigs Lemma if $A = mathbb{N}$ and $B = mathbb{B}$ (up to weak classical reasoning) GBI$_{A,B,T}$ intuitionistically captures the strength of $bullet$ G{o}dels completeness theorem in the form validity implies provability for entailment relations if $B = mathbb{B}$, $bullet$ bar induction when $A = mathbb{N}$, $bullet$ the Weak Fan Theorem when $A = mathbb{N}$ and $B = mathbb{B}$. Contrastingly, even though GDC$_{A,B,T}$ and GBI$_{A,B,T}$ smoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when $A$ is $mathbb{B}^mathbb{N}$ and $B$ is $mathbb{N}$.
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support e
In control theory, to solve a finite-horizon sequential decision problem (SDP) commonly means to find a list of decision rules that result in an optimal expected total reward (or cost) when taking a given number of decision steps. SDPs are routinely
Godels Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theor
We identify principles characterizing Solomonoff Induction by demands on an agents external behaviour. Key concepts are rationality, computability, indifference and time consistency. Furthermore, we discuss extensions to the full AI case to derive AIXI.
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning ta