Escreva no estilo da teoria dos números

19

Escreva uma declaração matemática, usando os símbolos:

  • There exists at least one non-negative integer(escrito como Equantificador existencial)
  • All non-negative integers(escrito como Aquantificador universal)
  • + (Adição)
  • * (multiplicação)
  • = (igualdade)
  • >, <(operadores de comparação)
  • &(e), |(ou),! (não)
  • (, )(para agrupar)
  • nomes de variáveis

que é equivalente à declaração

Existe um número racional a, de modo que π + e * a é racional.

(é claro, π=3,1415 ... é a constante matemática igual à circunferência dividida pelo diâmetro de um círculo e e=2,7182 ... é o número de Euler )

Você deve provar que sua afirmação é realmente equivalente à afirmação acima.

Obviamente, o caminho "mais curto" para fazer isso é provar a afirmação verdadeira ou falsa e, em seguida, responder com uma afirmação trivialmente verdadeira ou falsa, pois todas as afirmações verdadeiras são equivalentes entre si, assim como todas as afirmações falsas.

No entanto, o valor de verdade da afirmação dada é um problema não resolvido em matemática : nem sabemos se π+e é irracional! Portanto, impedindo a pesquisa matemática inovadora, o desafio é encontrar uma declaração equivalente "simples", provar sua equivalência e descrevê-la o mais brevemente possível.

Pontuação

E A + * = > < & |e !cada um adiciona 1 à pontuação. (e )não adicione nada à pontuação. Cada nome de variável adiciona 1 à pontuação.

Por exemplo, E x (A ba x+ba>x*(x+ba))pontuação 13 ( E x A ba x + ba > x * x + ba)

Menor pontuação ganha.


Nota:

Isenção de responsabilidade: Esta nota não foi escrita pelo OP.

  • Este não é um desafio do . As respostas não são necessárias para conter o código.
  • Isso é semelhante, mas não é, um desafio à , pois você precisa escrever uma declaração e provar que é equivalente a outra declaração.
  • Você tem permissão para enviar uma Ax x=xdeclaração trivialmente verdadeira (por exemplo, para todos os x, x = x ) ou uma declaração trivialmente falsa (por exemplo, para todos os x, x> x Ax x>x) se puder provar que a declaração acima é verdadeira / falsa.
  • Você tem permissão para usar símbolos adicionais (semelhante ao lema no golfe de prova), mas a pontuação será contada da mesma forma que você não os usa.
    Por exemplo, se você definir a => bcomo significante (!a) | b, cada vez que usar =>sua prova, sua pontuação aumentará 2.
  • Como as constantes não estão listadas nos símbolos permitidos, você não deve usá-las.
    Por exemplo: A declaração 1 > 0pode ser escrita como

    
    Forall zero: ( zero + zero = zero ) =>
    Forall one: ( Forall x: x * one = x ) =>
    one > zero
    

    na pontuação de 23. (lembre-se de que =>custa 2 por uso).

Dicas

  • Para usar constantes naturais, você pode fazer E0, 0+0=0 & E1, At 1*t=t &(para não precisar do =>que é mais expansivo); para números maiores que 1, adicione alguns 1's
l4m2
fonte
5
Eu gosto do conceito aqui, mas a afirmação é realmente difícil de escrever e eu ficaria impressionado com qualquer solução, independentemente da pontuação. Eu sugeriria usar algo mais simples para que mais pessoas participassem.
Xnor
1
Você precisa de uma declaração matemática equivalente à dada. Em que sentido eles devem ser equivalentes ? Se eu estiver correto, a afirmação dada é falsa. Portanto, é difícil entender sua equivalência com outras afirmações. Por exemplo, é equivalente a Existe um número racional a, de modo que i + e * a é racional (onde i é a unidade imaginária)?
Luis Mendo
1
Nota atual basta dizer You are allowed to submit a trivially-true (e.g., for all x, x = x Ax x=x) or a trivially-false statement (e.g., for all x, x > x Ax x>x) if you can prove the statement above is true/false.. A declaração está agora provado nem refutado, então eu realmente não me importo se o problema fica chato porque tal problema está resolvido
l4m2
1
A pergunta escrita parecia enterrar majoritariamente o lede e evitar explicar o que realmente está acontecendo, por isso escrevi uma pequena explicação nas notas (que a não trivialidade do desafio depende do valor de verdade atualmente desconhecido da afirmação) .
Lynn
I'd be impressed by any solution no matter the score. A pontuação foi apenas para apontar para aqueles que podem resolver este problema
l4m2

Respostas:

27

671

E a (a+a>a*a & (E b (E c (E d (A e (A f (f<a | (E g (E h (E i ((A j ((!(j=(f+f+h)*(f+f+h)+h | j=(f+f+a+i)*(f+f+a+i)+i) | j+a<e & (E k ((A l (!(l>a & (E m k=l*m)) | (E m l=e*m))) & (E l (E m (m<k & g=(e*l+(j+a))*k+m)))))) & (A k (!(E l (l=(j+k)*(j+k)+k+a & l<e & (E m ((A n (!(n>a & (E o m=n*o)) | (E o n=e*o))) & (E n (E o (o<m & g=(e*n+l)*m+o))))))) | j<a+a & k=a | (E l (E m ((E n (n=(l+m)*(l+m)+m+a & n<e & (E o ((A p (!(p>a & (E q o=p*q)) | (E q p=e*q))) & (E p (E q (q<o & g=(e*p+n)*o+q))))))) & j=l+a+a & k=j*j*m))))))) & (E j (E k (E l ((E m (m=(k+l)*(k+l)+l & (E n (n=(f+m)*(f+m)+m+a & n<e & (E o ((A p (!(p>a & (E q o=p*q)) | (E q p=e*q))) & (E p (E q (q<o & j=(e*p+n)*o+q))))))))) & (A m (A n (A o (!(E p (p=(n+o)*(n+o)+o & (E q (q=(m+p)*(m+p)+p+a & q<e & (E r ((A s (!(s>a & (E t r=s*t)) | (E t s=e*t))) & (E s (E t (t<r & j=(e*s+q)*r+t))))))))) | m<a & n=a & o=f | (E p (E q (E r (!(E s (s=(q+r)*(q+r)+r & (E t (t=(p+s)*(p+s)+s+a & t<e & (E u ((A v (!(v>a & (E w u=v*w)) | (E w v=e*w))) & (E v (E w (w<u & j=(e*v+t)*u+w))))))))) | m=p+a & n=(f+a)*q & o=f*r)))))))) & (E m (m=b*(h*f)*l & (E n (n=b*(h*f+h)*l & (E o (o=c*(k*f)*i & (E p (p=c*(k*f+k)*i & (E q (q=d*i*l & (m+o<q & n+p>q | m<p+q & n>o+q | o<n+q & p>m+q))))))))))))))))))))))))))

Como funciona

Primeiro, multiplique pelos denominadores comuns supostos de a e (π + e · a) para reescrever a condição como: existe a, b, c ∈ ℕ (nem todo zero) com a · π + b · e = c ou a · π - b · e = c ou −a · π + b · e = c. Três casos são necessários para lidar com problemas de sinal.

Então, precisamos reescrever isso para falar sobre π e e por aproximações racionais: para todas as aproximações racionais π₀ <π <π₁ e e₀ <e <e₁, temos a · π₀ + b · e₀ <c <a · π₁ + b · e₁ ou a · π₀ - b · e₁ <c <a · π₁ + b · e₀ ou −a · π₁ + b · e₀ <c <−a · π₀ + b · e₁. (Observe que agora obtemos a condição "nem todo zero" de graça.)

Agora, para a parte difícil. Como obtemos essas aproximações racionais? Queremos usar fórmulas como

2/1 · 2/3 · 4/3 · 4/5 ⋯ (2 · k) / (2 · k + 1) <π / 2 <2/1 · 2/3 · 4/3 · 4/5 ⋯ (2 · k) / (2 · k + 1) · (2 ​​· k + 2) / (2 · k + 1),

((k + 1) / k) k <e <((k + 1) / k) k + 1 ,

mas não há maneira óbvia de escrever as definições iterativas desses produtos. Então, construímos um pouco de maquinaria que descrevi pela primeira vez neste post do Quora . Definir:

divide (d, a): = ∃b, a = d · b,

powerOfPrime (a, p): = ∀b, ((b> 1 e divide (b, a)) ⇒ divide (p, b)),

que é satisfeito se a = 1, ou p = 1, ou p é primo e a é um poder disso. Então

isDigit (a, s, p): = a <p e ∃b, (powerOfPrime (b, p) e ∃qr, (r <be s = (p · q + a) · b + r))

é satisfeito se a = 0 ou a é um dígito do número da base-p s. Isso nos permite representar qualquer conjunto finito usando os dígitos de algum número base-p. Agora, podemos traduzir cálculos iterativos escrevendo, aproximadamente, que existe um conjunto de estados intermediários, de modo que o estado final está no conjunto, e cada estado no conjunto é o estado inicial ou segue em uma etapa de outro estado no conjunto.

Os detalhes estão no código abaixo.

Gerando código no Haskell

{-# LANGUAGE ImplicitParams, TypeFamilies, Rank2Types #-}

-- Define an embedded domain-specific language for propositions.
infixr 2 :|

infixr 3 :&

infix 4 :=

infix 4 :>

infix 4 :<

infixl 6 :+

infixl 7 :*

data Nat v
  = Var v
  | Nat v :+ Nat v
  | Nat v :* Nat v

instance Num (Nat v) where
  (+) = (:+)
  (*) = (:*)
  abs = id
  signum = error "signum Nat"
  fromInteger = error "fromInteger Nat"
  negate = error "negate Nat"

data Prop v
  = Ex (v -> Prop v)
  | Al (v -> Prop v)
  | Nat v := Nat v
  | Nat v :> Nat v
  | Nat v :< Nat v
  | Prop v :& Prop v
  | Prop v :| Prop v
  | Not (Prop v)

-- Display propositions in the given format.
allVars :: [String]
allVars = do
  s <- "" : allVars
  c <- ['a' .. 'z']
  pure (s ++ [c])

showNat :: Int -> Nat String -> ShowS
showNat _ (Var v) = showString v
showNat prec (a :+ b) =
  showParen (prec > 6) $ showNat 6 a . showString "+" . showNat 7 b
showNat prec (a :* b) =
  showParen (prec > 7) $ showNat 7 a . showString "*" . showNat 8 b

showProp :: Int -> Prop String -> [String] -> ShowS
showProp prec (Ex p) (v:free) =
  showParen (prec > 1) $ showString ("E " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (Al p) (v:free) =
  showParen (prec > 1) $ showString ("A " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (a := b) _ =
  showParen (prec > 4) $ showNat 5 a . showString "=" . showNat 5 b
showProp prec (a :> b) _ =
  showParen (prec > 4) $ showNat 5 a . showString ">" . showNat 5 b
showProp prec (a :< b) _ =
  showParen (prec > 4) $ showNat 5 a . showString "<" . showNat 5 b
showProp prec (p :& q) free =
  showParen (prec > 3) $
  showProp 4 p free . showString " & " . showProp 3 q free
showProp prec (p :| q) free =
  showParen (prec > 2) $
  showProp 3 p free . showString " | " . showProp 2 q free
showProp _ (Not p) free = showString "!" . showProp 9 p free

-- Compute the score.
scoreNat :: Nat v -> Int
scoreNat (Var _) = 1
scoreNat (a :+ b) = scoreNat a + 1 + scoreNat b
scoreNat (a :* b) = scoreNat a + 1 + scoreNat b

scoreProp :: Prop () -> Int
scoreProp (Ex p) = 2 + scoreProp (p ())
scoreProp (Al p) = 2 + scoreProp (p ())
scoreProp (p := q) = scoreNat p + 1 + scoreNat q
scoreProp (p :> q) = scoreNat p + 1 + scoreNat q
scoreProp (p :< q) = scoreNat p + 1 + scoreNat q
scoreProp (p :& q) = scoreProp p + 1 + scoreProp q
scoreProp (p :| q) = scoreProp p + 1 + scoreProp q
scoreProp (Not p) = 1 + scoreProp p

-- Convenience wrappers for n-ary exists and forall.
class OpenProp p where
  type OpenPropV p
  ex, al :: p -> Prop (OpenPropV p)

instance OpenProp (Prop v) where
  type OpenPropV (Prop v) = v
  ex = id
  al = id

instance (OpenProp p, a ~ Nat (OpenPropV p)) => OpenProp (a -> p) where
  type OpenPropV (a -> p) = OpenPropV p
  ex p = Ex (ex . p . Var)
  al p = Al (al . p . Var)

-- Utility for common subexpression elimination.
cse :: Int -> Nat v -> (Nat v -> Prop v) -> Prop v
cse uses x cont
  | (scoreNat x - 1) * (uses - 1) > 6 = ex (\x' -> x' := x :& cont x')
  | otherwise = cont x

-- p implies q.
infixl 1 ==>

p ==> q = Not p :| q

-- Define one as the unique n with n+n>n*n.
withOne ::
     ((?one :: Nat v) =>
        Prop v)
  -> Prop v
withOne p =
  ex
    (\one ->
       let ?one = one
       in one + one :> one * one :& p)

-- a is a multiple of d.
divides d a = ex (\b -> a := d * b)

-- a is a power of p (assuming p is prime).
powerOfPrime a p = al (\b -> b :> ?one :& divides b a ==> divides p b)

-- a is 0 or a digit of the base-p number s (assuming p is prime).
isDigit a s p =
  cse 2 a $ \a ->
    a :< p :&
    ex
      (\b -> powerOfPrime b p :& ex (\q r -> r :< b :& s := (p * q + a) * b + r))

-- An injection from ℕ² to ℕ, for representing tuples.
pair a b = (a + b) ^ 2 + b

-- πn₀/πd < π/4 < πn₁/πd, with both fractions approaching π/4 as k
-- increases:
-- πn₀ = 2²·4²·6²⋯(2·k)²·k
-- πn₁ = 2²·4²·6²⋯(2·k)²·(k + 1)
-- πd = 1²⋅3²·5²⋯(2·k + 1)²
πBound p k cont =
  ex
    (\s x πd ->
       al
         (\i ->
            (i := pair (k + k) x :| i := pair (k + k + ?one) πd ==>
             isDigit (i + ?one) s p) :&
            al
              (\a ->
                 isDigit (pair i a + ?one) s p ==>
                 ((i :< ?one + ?one :& a := ?one) :|
                  ex
                    (\i' a' ->
                       isDigit (pair i' a' + ?one) s p :&
                       i := i' + ?one + ?one :& a := i ^ 2 * a')))) :&
       let πn = x * k
           πn = πn + x
       in cont πn πn πd)

-- en₀/ed < e < en₁/ed, with both fractions approaching e as k
-- increases:
-- en₀ = (k + 1)^k * k
-- en₁ = (k + 1)^(k + 1)
-- ed = k^(k + 1)
eBound p k cont =
  ex
    (\s x ed ->
       cse 3 (pair x ed) (\y -> isDigit (pair k y + ?one) s p) :&
       al
         (\i a b ->
            cse 3 (pair a b) (\y -> isDigit (pair i y + ?one) s p) ==>
            (i :< ?one :& a := ?one :& b := k) :|
            ex
              (\i' a' b' ->
                 cse 3 (pair a' b') (\y -> isDigit (pair i' y + ?one) s p) ==>
                 i := i' + ?one :& a := (k + ?one) * a' :& b := k * b')) :&
       let en = x * k
           en = en + x
       in cont en en ed)

-- There exist a, b, c ∈ ℕ (not all zero) with a·π/4 + b·e = c or
-- a·π/4 = b·e + c or b·e = a·π/4 + c.
prop :: Prop v
prop =
  withOne $
  ex
    (\a b c ->
       al
         (\p k ->
            k :< ?one :|
            Bound p k $ n πn πd ->
               eBound p k $ \en en ed ->
                 cse 3 (a * πn * ed) $ \x ->
                   cse 3 (a * πn * ed) $ \x ->
                     cse 3 (b * en * πd) $ \y ->
                       cse 3 (b * en * πd) $ \y ->
                         cse 6 (c * πd * ed) $ \z ->
                           (x + y :< z :& x + y :> z) :|
                           (x :< y + z :& x :> y + z) :|
                           (y :< x + z :& y :> x + z))))

main :: IO ()
main = do
  print (scoreProp prop)
  putStrLn (showProp 0 prop allVars "")

Experimente online!

Anders Kaseorg
fonte
"que é satisfeito se a = 1, ou p é primo e a é uma potência dele" - você também pode ter p = 1. Embora p> 1 esteja implícito isDigit, o único local em que você o usa.
Ørjan Johansen
@ ØrjanJohansen Obrigado, corrigi essa nota. (Na verdade, não importa qual conjuntos powerOfPrimee isDigitacabam representando em casos inesperados, desde que haja alguma forma de representar cada conjunto finito.)
Anders Kaseorg
2
Se ativer pontuação 7 ou superior, acho, vale a pena adicionar um ex (\a' -> a' := a :& ... )invólucro isDigit.
Ørjan Johansen
@ ØrjanJohansen Claro, isso economiza 68. Obrigado!
Anders Kaseorg
Eu acredito que você precisa exigir k>0, pois eBoundfornece um denominador zero (e um numerador zero) no k==0caso, então todas as alternativas falham.
Ørjan Johansen
3

270

E1                                                                              { Exist 1, defined when Any k introduced }
Ec1 Ec2 Ec3 Ec4 Ec5 Ak k*1=k & c3>1 & ( En0 An n<n0 |                           { for large enough n, |(c1-c4)e+c3(4-pi)/8+(c2-c5)|<1/k }
Ex Ep Ew Emult At (Eb ((b>1 & Eh b*h=t) &! Eh h*p=b)) |                         { x read in base-p, then each digit in base-w. t as a digit }
Ee1 Ee2 Ehigher Elower e2<p & lower<t & ((higher*p+e1)*p+e2)*t+lower=x &        { last digit e1, this digit e2 }
    { Can infer that e2=w+1 | e1<=e2 & u1<=u2 & i1<=i2 & s1<=s2 & t1<=t2, so some conditions omitted }
Ei1 Es1 Et1 Eu1 (((u1*w)+i1)*w+t1)*w+s1=e1 &                                    { (u,i,t,s) }
Ei2 Es2 Et2 Eu2 i2<w & s2<w & t2<w & (((u2*w)+i2)*w+t2)*w+s2=e2 &               { e2=1+w is initial state u=i=0, s=t=1 }
(e2=w+1 | e1=e2 | i2=i1+1+1 & s2=s1*(n+1) & t2=t1*n &                           { i=2n, s=(n+1)^n, mult=t=n^n, s/mult=e }
Eg1 Eg2 g1+1=(i2+i2)*(i2+i2) & g1*u1+mult=g1*u2+g2 & g2<g1) &                   { u/mult=sum[j=4,8,...,4n]1/(j*j-1)=(4-pi)/8. mult=g1*(u2-u1)+g2 }
(t>1 | i2=n+n & t2=mult & Ediff Ediff2                                          { check at an end t=1 }
c1*s2+c2*mult+c3*u2+diff=c4*s2+c5*mult+diff2 & k*(diff+diff2)<mult))            { |diff-diff2|<=diff+diff2<mult/k, so ...<1/k }

a|b&c é a|(b&c) porque acho que remover esses parênteses faz com que pareça melhor, de qualquer maneira eles são gratuitos.

Utilizou JavaScript "(expr)".replace(/\{.*?\}/g,'').match(/[a-z0-9]+|[^a-z0-9\s\(\)]/g)para contar tokens.

l4m2
fonte
Por que você pode pegar mult = t? Além disso, como xsó pode ter muitos dígitos finitos, você precisará permitir e1 = e2 = 0que sejam suficientemente grandes t. Além disso, você precisará de mais parênteses ou outra desambiguação para construções ambíguas, como _ & _ | _.
Anders Kaseorg 25/10
@AndersKaseorg Eu multiplico cada item mult. Não vejo nenhum problema mult=t2no final. e1=e2=0deve ser corrigido, mas não tão certo, então, atualmente, não mudo a aceitação.
l4m2
Se a & b | cfor, (a & b) | centão você t*1=testá definitivamente no lugar errado. Além disso, você não excluiu a solução trivial c1 = c4 & c2 = c5 & c3 = 0 & diff = diff2.
Anders Kaseorg 25/10
@AndersKaseorg Minha razão por que diff≠diff2trabalhar?
l4m2
De qualquer forma, eu posso usar !(c2=c5)como já sabemos que eé irracional, portanto, mesmo que isso não funcione, a pontuação não aumentará
l4m2 26/10