В этой статье я попробую показать соотвествие между между математическими доказательствами и программами, а так же попытаюсь ненавязчиво ввести читателя в синтаксис Agda.

#agda

И да, эта статья тоже будет типо DRAFT и я ее буду дополнять.

Соответствие Карри-Ховарда устанавливает соответствие между типизированным лямбда исчислением и интуиционистской логикой. Типы соответствуют высказываниям. Если мы построим значение определённого типа, то мы так же докажем высказываение соответствующее этому типу. Поскольку типы являются высказываниями, а значения являются доказательствами, конструкторы для типа соответствуют правилам вывода для соответствующего предположения.

В таблице ниже соответствие представлено более наглядно:

Логические системы	Языки программирования
Высказывание	Тип
Доказательство высказывания P	Терм(выражение) типа P
Утверждение P доказуемо	Тип P обитаем(∃ p ∈ P)
Импликация P ⇒ Q	Функциональный тип P → Q
Конъюнкция P ∧ Q	Тип произведения(пары) P × Q
Дизъюнкция P ∨ Q	Тип суммы (размеченного объединения) P + Q
Истинная формула	Единичный тип (⊤)
Ложная формула	Пустой тип (⊥)
Квантор всеобщности ∀	Тип зависимого произведения (Π-тип)
Квантор существования ∃	Тип зависимой суммы (Σ-тип)

Модули

Определим модуль:

{-# OPTIONS --safe #-}
module CurryHoward where

Имя модуля на верхнем уровне должно соответствовать названию файла, а вложенные модули могут называться как угодно или даже не иметь названия. Тут так же могут быть указаны опции компилятора, например, очень частая опция —safe заставляет компилятор убедиться, что выключены другие опции, которые могут вызывать противоречия и отключает возможность делать постулаты, а так же проверяет, что все импорты тоже “безопасны”.

Единичный тип

Определим единичный тип как тип с одним конструктом:

data ⊤ : Set where 
    tt : ⊤ 

(подробнее про объявление типов)

Пустой тип

Определим пустой тип как тип без конструкторов:

data ⊥ : Set where 

Здесь же определим элиминатор пустоты

⊥-elim : ∀ {A : Set}  → ⊥ → A  
⊥-elim () -- это так называемый absurd pattern, который можно использовать когда нет ни одного значения которое можно было бы передать в эту функцию

(подробнее про Absurd Pattern)

Определим отрицание, отрицание для типа A будет означать функцию которая A в пустой тип ⊥

¬_ : Set → Set 
¬ A = ⊥

Функциональный тип как импликация

Определим функциональный тип и покажем, что он соотвествует импликации:

-- true ⇒ true 
f₁ : ⊤ → ⊤ 
f₁ tt = tt 

-- false ⇒ true 
f₂ : ⊥ → ⊤ 
f₂ _ = tt 

-- false ⇒ true можно так же доказать через элиминатор пустоты
f₂' : ⊥ → ⊤ 
f₂' x = ⊥-elim x 

-- false ⇒ false 
f₃ : ⊥ → ⊥ 
f₃ x = x 

-- true ⇒ false невозможно определить т.к. нет способа сконструировать пустой тип
-- f₄ : ⊤ → ⊥ 
-- f₄ = ？ 

-- ¬ true тоже невозможно определить т.к. нет способа сконструировать пустой тип
-- f₄' : ¬ ⊤ 
-- f₄' = ？ 

Ну и давайте на пример тавтологии A ⇒ (B ⇒ A) покажем как можно использовать явный и не явный полиморфизм

-- Явным образом
taut : (A B : Set) → A → (B → A) 
taut T₁ T₂ t₁ t₂ = t₁ 

-- Вызывать придется с явным указанием типов 
taut-ex : ⊥ → (⊥ → ⊥)
taut-ex = taut ⊥ ⊥ 

-- Эквивалентная запись 
taut₂ : (A : Set)(B : Set) → A → (B → A) 
taut₂ T₁ T₂ t₁ t₂ = t₁ 

-- Эквивалентная запись 
taut₃ : (A : Set) → (B : Set) → A → (B → A) 
taut₃ T₁ T₂ t₁ t₂ = t₁ 

-- Так же можно добавлять квантор всеобщности 
taut₄ : ∀ (A : Set) → (B : Set) → A → (B → A) 
taut₄ T₁ T₂ t₁ t₂ = t₁ 

-- Эквивалентная запись 
taut₅ : ∀ (A B : Set) → A → (B → A) 
taut₅ T₁ T₂ t₁ t₂ = t₁ 

-- Неявный образом
taut' : {A B : Set} → A → (B → A) 
taut' t₁ t₂ = t₁ 

-- Тогда типы можно передать или не передавать
taut'-ex₁ : ⊥ → (⊥ → ⊥)
taut'-ex₁ = taut' {⊥} {⊥} -- передаются неявные параметры в фигурных скобках, если нужно

-- Или передать один, причем можно указать какой
taut'-ex₂ : {A : Set} → A → (⊥ → A)
taut'-ex₂ = taut' {B = ⊥}

-- В целом можно делать все тоже самое, что и с круглыми скобками -- добавлять стрелочки и квантор всеобщности, и даже получать неявные параметры и использовать их в функции
taut'₂ : {A : Set} → ∀ {B : Set} → A → (B → A) 
taut'₂ {B = T₂} t₁ t₂ = t₁ --тут можно использовать T₂

-- Если совсем безумствовать, то с ума можно сходить очень по разному
taut'₃ : ∀ (A : Set) → {B : Set} → A → (B → A) 
taut'₃ T₁ t₁ t₂ = t₁ 

-- Вообще-то даже Set можно не писать, если писать ∀, но в таком общем коде лучше писать(можно смело писать, где из контекста понятен конкретный тип) 
-- т.к. там есть нюансы с вложенностью типов в типы
taut'₄ : ∀ A → ∀ {B} → A → (B → A) 
taut'₄ T₁ = λ t₁ t₂ → t₁ --а еще лямбды можно писать

(еще подробнее про объвление функций)

Тип произведения (пары)

Определим тип пары, который соотвествует коньюнкции

data _×_ (P : Set) (Q : Set) : Set where
    pair : P → Q → (P × Q)

И тогда можно показать, что

-- P ∧ Q ⇒ P
×-elim₁ : {P Q : Set} → (P × Q) → P
×-elim₁  (pair p _) = p

-- P ∧ Q ⇒ Q
×-elim₂ : {P Q : Set} → (P × Q) → Q
×-elim₂  (pair _ q) = q

Тип суммы

Определим тип суммы, который соотвествует дизъюнкции

data _+_ (P Q : Set) : Set where
   Left : P → P + Q
   Right : Q → P + Q

И тогда можно показать, что

+-elim : {A B C : Set} → (A → C) → (B → C) → (A + B) → C
+-elim ac bc (Left a) = ac a
+-elim ac bc (Right b) = bc b

Сигма тип(зависимая сумма)

А вот сейчас будет сложно. Во первых, потому что зависимые типы, во вторых, мы незаметно введем уровни для типов Set(в целом все что нужно знать это Set i имеет тип Set (i + 1), сделано так, чтобы обойти парадокс Рассела), а в третьих, сумма это теперь пара, т.е. фактически зависимая сумма это обобщение произведения, и понимайте это как хотите(если я сам это когда-нибудь осознаю обязательно расскажу).

open import Agda.Primitive

record Σ {i j} (A : Set i) (P : A → Set j) : Set (i ⊔ j) where 
  constructor _,_
  field
    fst : A    
    snd : P fst 

(подробнее про record'ы и про уровни)

В стандартной билиотеке есть еще несколько удобных синтаксисов для Σ-типа

Σ-syntax : ∀ {a}{b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

∃ : ∀ {a}{b}{A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

∃-syntax : ∀{a}{b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃-syntax = ∃

syntax ∃-syntax (λ x → B) = ∃[ x ] B

Фактически Σ-тип можно воспринимать как значение типа A и зависящий от этого значения предикат P. Например

-- Для любого типа B существует тип A такой, что существует функция B → A
Σ-ex : ∀ {B} → Σ Set (λ A → B → A)
Σ-ex = ⊤ , λ _ → tt

-- Или тоже самое используя синтаксис Σ
Σ-ex' : ∀ {B} → Σ[ A ∈ Set ] (B → A)
Σ-ex' = ⊤ , λ _ → tt

-- Или тоже самое используя синтаксис ∃
Σ-ex'' : ∀ {B} → ∃[ A ] (B → A)
Σ-ex'' = ⊤ , λ _ → tt

Пи тип(зависимое произведение)

Пи-тип, он же тип зависимой функции, он же тип зависимого произведения, можно использовать и без дополнительных определений т.к. фактически он зашит в Agda, но чисто формально его можно представить так:

Π : ∀ { n m }(A : Set n)(P : A → Set m) → Set(m ⊔ n)
Π A P = (x : A) → P x

Тип Π можно воспринимать как квантор всеобщности где для любого элемента типа A истинен предикат P. Например:

--Для любого типа существует функция из него в непустое множество
Π-ex : Π Set (λ A → A → ⊤)
Π-ex = λ _ _ → tt

Зависимые типы

Зависимые типы это одна из ключевых фишек Agda позволяющая конструировать функции в которых типы зависят от термов или даже типы от типов, данные типы можно воспринимать в том числе как предикаты или отношения, а их обитаемость как доказательства свойств термов.

Например, можно определить равенство Лейбница, когда x = y, если для любого предиката P: P x = P y.

_==_ : ∀ {A : Set} (x y : A) → Set₁
_==_ {A} x y = Π (A → Set) (λ p → (p x → p y))
-- определение эквивалентно ∀ (P : A → Set) → P x → P y

и тогда можно показать рефлексивность ==

refl-== : ∀ {A : Set}{x : A} → x == x
refl-== P Px = Px

На самом деле в Agda равенство термов и типов обычно определяется иначе, но кажется это хороший пример, чтобы показать как работают зависимые типы.

Вместо послесловия

Надеюсь было не слишком абстрактно, специально не хотелось вводить дополнительные типы, чтобы сконцентрироваться именно на соответствии логических операций и типов. Далее, возможно, хотелось бы разобрать такую штуку как Decidability т.к. иногда нужно с уровня типов опуститься на уровень термов, чтобы, например, факт обитаемости того или иного типа сопоставить с true и false, как это было в статье про лямбда исчисление в if_then_else

Используемые символы и их коды:

Символ	Код
→	\to
∧	\and
∨	\or
λ	\lambda
∣ ∈	\in
∃	\exists
×	\x
∣ ⊤	\top
⊥	\bot
∀	\forall
Π	\Pi
Σ	\Sigma
⇒	\=>
ₙ	\_n

Эта статья будет публичной, но в статусе DRAFT, скорее всего я буду ее дополнять и пересматривать, пока тут какие-то базовые определения и доказательство того, что у (λx.xx)(λx.xx) нет нормальной формы. Скорее всего тут есть некоторые неточности и даже ошибки, буду исправлять в процессе.

#agda #lambdacalculus

Определим модуль и импортируем необходимые модули

module LambdaCalc where

open import Data.Nat
open import Data.Bool hiding (_≟_)
import Relation.Binary.PropositionalEquality as Eq
open Eq hiding (subst)
open Eq.≡-Reasoning
open import Relation.Nullary.Decidable 
open import Data.Empty using (⊥; ⊥-elim) 
open import Data.Unit using (⊤; tt) 
open import Data.Product

Начнем с определения термов лямбда-исчисления. Для простоты будем использовать индексы де Брауна для переменных, это когда переменные не именуются, а нумеруются (индексируются), индекс показывает, сколько лямбд назад переменная была связана:

λx. (λy. x y) ↔ λ (λ 1 0) λx. x (λy. x y y) ↔ λ 0 (λ 1 0 0)

-- Определение термов лямбда-исчисления
data Λ : Set where     
  _`  : ℕ → Λ          -- Переменная
  λ'_  : Λ → Λ         -- Лямбда-абстракция 
  _∘_  : Λ → Λ → Λ     -- Применение 

Подстановка нужна для реализации бета-редукции:

-- Подстановка терма вместо переменной
subst : Λ → ℕ → Λ → Λ 
--Если переменная равна той же вместо которой мы подставляем, то подставляем, иначе не подставляем
--Как работают ⌊_⌋ и ≟ надо будет как-нибудь объяснить, но пока поверьте, что это такое хитрое сравнение на равенство
subst (x `) y s = if ⌊ x ≟ y ⌋ then s else (x `)
--Внутрь лямбда абстрации тоже можем подставить(увеличиваем на единицу значение искомого индекса т.к. погружаемся глубже)
subst (λ' t) y s = λ' (subst t (suc y) s)
--Можем подставить с обеих сторон применения
subst (t ∘ u) y s = (subst t y s) ∘ (subst u y s)

Теперь определим одношаговую бета-редукцию:

-- Одношаговая бета-редукция
data _→β_ : Λ → Λ → Set where
  --Если есть абстракция и применение, то можем применить подстановку
  beta : ∀ {t u} → ((λ' t) ∘ u) →β (subst t 0 u)
  --Можно редуцировать левую часть применения
  app₁ : ∀ {t t' u} → t →β t' → (t ∘ u) →β (t' ∘ u)
  --Можно редуцировать правую часть применения
  app₂ : ∀ {t u u'} → u →β u' → (t ∘ u) →β (t ∘ u')
  --Можно редуцировать под лямбда абстракцией
  lam  : ∀ {t t'} → t →β t' → (λ' t) →β (λ' t')

Определяем многошаговую редукцию:

-- Многошаговая редукция (→β*)
data _→β*_ : Λ → Λ → Set where
  refl : ∀ {M} → M →β* M
  step : ∀ {M N P} → M →β N → N →β* P → M →β* P

Определяем нормальную форму:

Normal : Λ → Set
--Переменная уже в нормальной форме
Normal (x `)    = ⊤
--Если есть лямбда абстракция и применение к ней, то это редекс т.е. можно использовать подстановку
Normal ((λ' _) ∘ _) = ⊥
--Применение имеет нормальную форму, если оба аргумента имеют нормальную форму
Normal (M ∘ N)  = Normal M × Normal N
--Лямбда абстракция имеет нормальную форму, если терм внутри имеет нормальную форму
Normal (λ' M)    = Normal M

-- Определение Ω = (λx.xx)(λx.xx)
Ω : Λ
Ω = (λ' ((0 `) ∘ (0 `))) ∘ (λ' ((0 `) ∘ (0 `)))

--xx не редуцируется
l1 : ∀ {x t} → ((x `) ∘ (x `)) →β t → ⊥ 
l1 (app₁ ())  --интересно, кстати, почему этого кейса достаточно и Agda не требует еще разобрать app₂
--() это так называемый absurd pattern, т.е. не существует такой β-редукции, которую мы могли бы применить к левой части применения

--λx.xx не редуцируется 
l2 : ∀ {x t} → (λ' ((x `) ∘ (x `))) →β t → ⊥ 
l2 (lam b) = l1 b

--(λx.xx)(λx.xx) редуцируется в себя
l3 : Ω →β Ω 
l3 = beta

--Ω всегда редуцируется в Ω
Ω→βΩ : ∀ T → Ω →β T → T ≡ Ω
--Если использовать применение, то Ω переходит в себя по определению
Ω→βΩ t beta = refl
--Если мы редуцировали левую часть применения, то это могла быть только λx.xx, что невозможно
Ω→βΩ _ (app₁ b) = ⊥-elim (l2 b)
-- А вот тут почему-то требует app₂ проверить :) 
Ω→βΩ _ (app₂ b) = ⊥-elim (l2 b)

Ну и собственно доказываем, что у Ω нет нормальной формы

--У Ω нет нормальной формы
no-normal-form : ∀ {N} → Ω →β* N → Normal N → ⊥ 
--Тут это другой refl из многошаговой β-редукции
no-normal-form refl ()
--Если это была редукция, то Ω перешла в себя
no-normal-form (step beta steps) nf = no-normal-form steps nf
--Остальные варианты невозможны
no-normal-form (step (app₁ t) steps) nf = l2 t
no-normal-form (step (app₂ t) steps) nf = l2 t

Используемые символы и их коды:

Символ	Код
→	\to
Λ	\Lambda
λ	\lambda
⊤	\top
⊥	\bot
ℕ	\bN
∘	\o
∀	\forall
⌊	\clL
⌋	\clR
≟	\?=
₁	_1
₂	_2
β	\beta
Ω	\Omega

Die beiden tragischen Anschläge in Magdeburg und Aschaffenburg werden derzeit auf perfide Weise von den rechtsaußen Parteien emotionalisiert und instrumentalisiert, obwohl die Eltern der Opfer darum gebeten haben, dies nicht zu tun. Dabei werden die Rechten mit Nachdruck von diversen Medien unterstützt, die bereits eine lange Tradition der Brandstiftung pflegen. Mittlerweile gesellt sich auch der ÖRR immer mehr dazu. Ob aus vorauseilendem Gehorsam, oder weil die rechtsextremen Parolen in den Redaktionen auch immer mehr verfangen, lässt sich nur noch schwer unterscheiden. Das Narrativ, das Migration gerade unser allergrößtes Problem sei und der Untergang des Abendlandes drohe, plättet gerade sämtliche anderen Themen und Probleme in der Berichterstattung. Wahlkampf sei Dank. Wohnungsnot, Klimakrise, Inflation und Armut, Ukraine-Krieg usw., spielt gerade alles keine Rolle. Die Angst frisst den Verstand auf.

Es sollte jedem klar sein, dass es den Rechten nicht vorrangig um die Begrenzung der Migration geht, sondern sie wissen, dass sie bei der Wahl der “illegalen Migranten” als Feindbild sehr wahrscheinlich eine große Zustimmung in der Bevölkerung bekommen. Sicherheit ist ein menschliches Grundbedürfnis, und die Angst diese zu verlieren ist so tief verankert, dass sie sich extrem leicht von Populisten nutzen lässt, um viele Menschen zu manipulieren. Der Wunsch nach einfachen Lösungen in einer immer komplexer werdenden Welt, bietet den Haudrauf-Maulhelden in der Politik zusätzlich eine Klaviatur, die sie gerne bespielen.

Wenn ihnen dieser Schritt der Migrationsbegrenzung gelingt, inklusive der weiteren Normalisierung rechtsextremer Positionen, können sie das als Sprungbrett nutzen,um ihre Macht weiter auszubauen. Und dann sind sehr bald die bereits hier legal lebenden Menschen mit Migrationshintergrund dran. Danach vielleicht Kranke, Behinderte, Homosexuelle, und irgendwann auch Journalisten, Lehrer, Wissenschaftler, Intellektuelle und andere Gruppen, die nicht in die völkisch-nationale Ideologie hineinpassen.

Die Idee, dass Freiheit immer die Freiheit der Andersdenkenden ist, ist mit faschistischer Ideologie nicht vereinbar.

In was für einer Gesellschaft wollen wir leben?

Einer Gesellschaft, die das Grundgesetz, die Menschenrechte und ein solidarisches Miteinander wertschätzt? Oder einer Gesellschaft, in der das Recht des Stärkeren gilt?

In einer Gesellschaft, die sich durch die Einflüsse anderer Kulturen bereichert und beschenken lässt und über den Tellerrand hinausschaut? Oder in einer Gesellschaft, die sich abschottet und alles Fremde als minderwertig ansieht?

Das Problem heißt Rassismus, und dieser zieht sich systematisch durch die Strukturen im Land. Alle Regierungen der letzten Jahrzehnte haben nicht die nötigen Schritte unternommen, um Migration und Integration menschenwürdig zu gestalten. Stattdessen wurde das Asylrecht immer weiter verschärft, aus Angst vor zunehmender Gewalt von rechts. Der latente Rassismus in unserer Gesellschaft hat dafür gesorgt, dass wir unzureichende Strukturen haben, die letztlich die Probleme verursachen, die wiederum Wasser auf die Mühlen der Menschenfeinde sind. 2015 wäre eine Chance gewesen, grundlegende und nachhaltigere Struktur-Änderungen zu schaffen. Frau Merkels “Wir schaffen das” war damals ein wichtiger Impuls, aber nicht nachhaltig. Die meiste Arbeit wurde vor Ort von Freiwilligen in den Kommunen aufgefangen.

Natürlich schafft Migration auch Probleme und sorgt für Konflikte, sei es bei der Wohnungssuche oder anderweitig. Und das sind Probleme, die es zu lösen gilt. Aber Migration an sich ist nicht das Problem.

Dieses Narrativ gilt es zu durchbrechen, wenn wir nicht sehr bald in einem Land aufwachen wollen, in dem auch die Nicht-Migranten nicht mehr in Würde und Freiheit leben können.

---

Diskussion ist in diesem Thread möglich: https://social.tchncs.de/@marcr/113925349963168208

Wie holen wir uns die Zukunft zurück?

Der seltsame Retro-Fetischismus des Trumpismus/Elonismus – und was wir dem entgegensetzen können

Vom allgemeinen Zukunftsoptimismus der 1950er und 1960er Jahren sind wir in der westlichen Welt heute weit entfernt. Mein Eindruck ist, dass es viele Menschen in den westlichen Ländern gibt, die das Gefühl haben, dass wir in einem Jahrzehnt des Übergangs leben: Das Alte, die etablierte Wohlstandsordnung nach dem Zweiten Weltkrieg, ist vorüber – aber das Neue ist noch nicht da.

Auch die politische Weltlage passt in dieses Bild: Der aktuelle US-Präsident Donald Trump ist 1946 geboren und damit im selben Jahr wie Bill Clinton, der 1993 zum Präsidenten gewählt wurde.

Mit ihm ist ein eigentümliches Programm gewählt worden: Unterstützt von Milliardären wie Elon Musk und Peter Thiel, der 2009 ausführte, dass er nicht mehr daran glaube, dass Freiheit und Demokratie kompatibel seien. Damals forderte Thiel, Libertäre wie er sollten sich von Staaten abwenden und ihre eigenen Strukturen auf den Weltmeere, im Weltraum oder Cyberspace aufbauen. Inzwischen scheint er einen anderen Plan zu verfolgen: Statt neue libertäre Anti-Staaten zu gründen, in denen Superreiche ungestört von Steuern und Solidarität leben können, sollen die USA nach seinen Vorstellungen umgeformt werden.

Stilistisch und Ästhetisch fällt auf, dass das Trump-Lager nicht einmal den Versuch unternommen hat, eine Zukunftsvision zu kommunizieren. „Make America Great Again” bezieht sich auf die Vergangenheit – und daraus wurde auch ästhetisch kein Hehl gemacht. Der Wählerschaft wird Trump als ein zurück in die USA der 1950er bis 1980er verkauft, wie nostalgische Wahlkampfvideos des Trump-Lagers zeigen.

Trump-Wahlkampfvideo „National Revival”, unter anderem von Elon Musk verbreitet

Was also hatten die 1950er bis 1980er, das sie als Sehnsuchtsort so attraktiv macht? Vielleicht auch eine Vision einer besseren Zukunft, eines besseren Lebens für alle. Nicht nur die politische Rechte scheitert daran, eine Vision für die Zukunft anzubieten, weshalb sie uns eine Reise in die Vergangenheit als nationales Wiederaufblühen verkauft. Auch Liberale und Linke haben es seit Jahrzehnten nicht geschafft, eine Vision zu zeichnen, hinter der sich Menschen versammeln, die zusammenschweißt und Menschen das Gefühl gibt, mit ihrem Einsatz zu einem besseren Morgen beizutragen.

Seit Helmut Schmidts berühmten Satz „Wer Visionen hat soll zum Arzt gehen“ hat ihn niemand so sehr mit Leben gefüllt wie Ex-Kanzlerin Angela Merkel. Sie hat nicht geführt, sondern verwaltet. Und Olaf Scholz hat es geschafft, dieses Erbe noch einmal zu übertrumpfen. Merkel und Scholz waren Anti-Kennedys, dessen wohl berühmteste Sätze neben „Ich bin ein Berliner“ die folgenden waren:

„We choose to go to the Moon in this decade and do the other things, not because they are easy, but because they are hard; because that goal will serve to organize and measure the best of our energies and skills, because that challenge is one that we are willing to accept, one we are unwilling to postpone, and one we intend to win, and the others, too.“ John F. Kennedy

Was also könnte ein Bild einer lebenswerten Zukunft und Vision sein? „Eine Zukunft, in der man nur etwas später stirbt und bis dahin mehr Fahrrad fährt, ist keine“ zitiert DIE ZEIT den deutsch-österreichischen Journalisten und Autor Wolf Lotter. Die Vision, die der Autor des Artikels, Ulrich Machold, uns anbietet, klingt sehr bescheiden. „Ein Land, das wieder funktioniert, von Zügen bis zu Bürgerämtern, und das zumindest in der Nähe des technisch neuesten Stands der Dinge. Ein Land, das keine Panikattacke bekommt, wenn der Verbrennungsmotor vom Fortschritt überholt wird, weil es auch andere Stärken hat.“

Vielleicht ist eine bescheidene Vision auch besser als gar keine.

Hier wird gemeinsam die Predigt von Bischöfin Mariann ins Deutsche übertragen. https://pad.gwdg.de/50UqgfbOQaCbU4ArQqnPXA

#fedikirche

2 Tassen Mehl ¾ Tasse Wasser 2 El Olivenöl 1 Tl Salz Kneten, teilen in 12 kleine Bällchen, sehr dünn ausrollen, auf Backpapier oder Backfolie bei 240° ca. 5-7min backen.  Zum Teilen mit anderen

Ulrike Leininger

Gottes Segen komme zu uns Frauen, dass wir stark sind in unserer schöpferischen Kraft, dass wir mutig sind in unserem Recht. dass wir Nein sagen, wo es nötig ist, dass wir Ja sagen, wo es gut ist. Gottes Segen komme zu uns Frauen, dass wir schreien, wo Unrecht ist, dass wir schweigen, wo Entsetzen ist. Gottes Segen komme zu uns Frauen, dass wir Weisheit suchen und finden, dass wir Klugheit zeigen und geben. Gottes Segen komme zu uns Frauen, dass wir die Wirklichkeit verändern, dass wir das Lebendige fördern. Dass wir Gottes Mitstreiterinnen sind auf Erden.

(Hanna Strack)

Filmtipp https://www.arte.tv/de/videos/118580-000-A/zeitenwende-im-vatikan/

(Tschuldigung für diese bescheuerte Überschrift. Ich hatte gerade einen Cheech und Chong-Moment...)

Wow. Bald drei Monate bin ich schon von Mastodon weg! Nach etwa 17 Jahren in sozialen Netzwerken. Also Twitter und dem Fediversum. Ich möchte euch kurz mitteilen, was das mit mir gemacht hat:

Als ich relativ spontan mein Ende in den sozialen Netzwerken beschloss, wusste ich absolut nicht, was darauf hin passieren wird. Ich dachte, ich würde richtig viel bloggen. Nun, ich lag ganz großartig daneben. Statt zu bloggen, entdeckte ich das Lesen wieder und habe in fast drei Monaten mehr Bücher gelesen als in den vergangenen 17 Jahren zusammen. Ich liebe und genieße das Lesen. Und zwar sehr. Und mir wird klar, wie diese sozialen Netzwerke meine eh schon zerkratze Fokus-Fähigkeit gebunden haben.

Ich mülle mich nicht mehr mit Informationen zu. Soziale Netzwerke sind ein prima Medium, um sich den ganzen Dreck dieser Welt ungewollt um die Ohren schlagen zu lassen. Sowas macht etwas mit der Psyche. Seit ich mich bei Mastodon verabschiedet habe, bin ich wesentlich ausgeglichener, in mir ruhender, spüre mich mehr und habe insgesamt mehr Energie. Klar, damit ist der Dreck in dieser Welt zwar nicht weg, aber das wäre er auch nicht, wenn ich meinen Geist weiterhin damit weiterhin vollmüllen lassen würde.

Mein Klapprechner, der fast ununterbrochen lief, setzt Staub an. Ich starte das Ding nur noch, wenn ich wirklich was damit machen muss, etwas, was ich nicht am Handy erledigen kann. Und mein Handy ist momentan nur noch ein internetfähiger Musikplayer, auf dem ich Podcasts höre, hin und wieder ein paar abonnierte YouTube-Inhalte anschaue und kurz Dinge nachschlage oder mit dem ich meine Mails checke. Was das Strom spart! ;–)

Achso, ich habe aufgehört, in Tröts zu denken. Ehrlich, das habe ich gemacht, wenn ich etwas gesehen oder erlebt habe, von dem mir klar war, dass ich es meiner Bubble mitteilen will. Ich habe das Erlebte sofort in 500 Zeichen verpackt. Und natürlich ein Foto gemacht. Es fühlte sich etwas sehr strange an, als mir klar wurde, wie sehr dieses Mastodon zu meiner zweiten Natur und der Erdrandbewohner zu meiner Identität geworden war...

Was ich aber wirklich vermisse, ist der Austausch mit meiner wunderbar klugen neurodivergenten Timeline. Hierfür gibt es keinen Ersatz. Das Fehlen dieser virtuellen Verbundenheit mit meinen “Neurogeschwistern” hinterlässt ein Loch, das mich tatsächlich schmerzt.

Wie gehts weiter? Ich habe mir ja offengelassen, ob ich ins Fediversum zurückkehre oder auch nicht. Ich glaube, ich habe da eine Idee, die ich so umsetzen werde: Ich werde projektbezogen tröten. Meine Liebste und ich fahren bald für ein paar Tage nach Paris. Ich werde euch mitnehmen und von dieser Februar-Reise berichten. Darauf freue ich mich. Und im Mai folgt eine Reise nach London. Auch dahin nehme ich euch mit!

Abgesehen davon versuche ich ein wenig mehr zu bloggen. Vielleicht über Bücher? Wer weiß...

Bis bald!

Hier noch mein derzeitiges Lieblingslied, eine besondere Perle aus den Tiefen einer spinnwebenverhangenen Gruft. https://bleibmodern.bandcamp.com/track/winter-mood

Chaos is gut

Chaos macht Angst aber Chaos ist auch eine Chance.

Der brennende, sehnende, fühlende Mensch will an den Rand des inneren Chaos geführt werden, um die Chance zu bekommen – abseits der ausgetretene Pfade der „Normalen“ – es zu ordnen. Nicht nach den Normen des Außens, sondern nach dem Kompass des Inneren – dem Grundgefühl, dem schon immer geahnten Schicksal.

Diejenigen, die den Rand des inneren Chaos nie erreichen fühlen sich nicht selten als hätten sie ihr Leben schon gelebt, bevor es ganz vorbei ist.

Mariann Edgar Budde ist die anglikanische Episkopalbischöfin von Washington.

Ein ikonisches Foto

https://www.pro-medienmagazin.de/wp-content/uploads/2025/01/503345825-scaled-e1737560611395-1000x562.jpg

Die Predigt

• https://www.lessentiel.lu/de/video/washington-national-cathedral-trump-missfaellt-kritische-predigt-der-bischoefin-mariann-103264409
• https://www.ref.ch/news/mariann-budde-donald-trump-us-wahlen-bischofin-bischof-washington-glaube-kirche-barmherzigkeit/
• https://www.evangelisch.de/inhalte/238567/23-01-2025/bischoefin-bietet-trump-paroli-so-reagiert-die-community-auf-buddes-predigt
• https://www.katholisch.de/artikel/59033-bischoefin-budde-eine-standpauke-fuer-trump-umsonst

For those who are doubting themselves: Sing, let your heart soar, sing forever Sad and so happy, feelings flow over, now Our world is full of all kinds of colors Closing my eyes, I still can see the stars …. Flowers are blooming, oh, it’s beautiful Sing, sing, sing! — Belle, Million Miles Away

TEMA Golf ist Ihr Experte für individuelle und Gruppen-Golfreisen weltweit. Unser erfahrenes Team bietet maßgeschneiderte Lösungen, um unvergessliche Erlebnisse auf den schönsten Golfplätzen dieser Welt zu garantieren. Mit unserem Fokus auf Qualität und Flexibilität sorgen wir für einzigartige Golfreisen. Entdecken Sie mit uns die Welt des Golfsports!

Einzigartiges Abenteuer: Golfreise Südafrika

Südafrika ist eine außergewöhnliche Golfdestination, die durch ihre atemberaubenden Landschaften, erstklassigen Golfplätze und faszinierende Tierwelt begeistert. Von den Küsten des Westkaps bis hin zu den majestätischen Drakensbergen bietet das Land eine unvergleichliche Vielfalt an Golfplätzen, die Spieler aller Niveaus beeindrucken.

Berühmte Anlagen wie der Gary Player Country Club und Leopard Creek verbinden anspruchsvolle Spielbedingungen mit spektakulären Aussichten auf die afrikanische Wildnis. Neben dem Golfen haben Besucher die Möglichkeit, unvergessliche Safaris zu erleben, Weinproben in den besten Weingütern der Region zu genießen oder historische Städte wie Kapstadt zu erkunden.

Ihre Golfreise Südafrika wird zu einer perfekten Mischung aus sportlicher Herausforderung, kulturellen Entdeckungen und luxuriöser Entspannung. Südafrika bietet Golfern ein einzigartiges Erlebnis, das Natur, Abenteuer und Golfgenuss auf höchstem Niveau vereint.

Lassen Sie sich von der Magie dieses Landes verzaubern und erleben Sie eine Golfreise, die Sie nie vergessen werden. Von der spektakulären Tierwelt bis zu erstklassigen Golfplätzen ist Südafrika eine Destination, die jeden Golfliebhaber begeistern wird.